Mathematical Logic and Software Verification Joint Workshop

Mathematical Logic and Software Verification Joint Workshop

Date: 
2015/12/03 (Thu) to 2015/12/04 (Fri)
Place: 
Hotel Arrowle, Kaga
Group: 
Research Center for Software Verification
Thursday, December 03
13:00 - 13:10 Opening
Kazuhito Ogata
13:10 - 13:50 Recent Developments on Specification and Verification with CafeOBJ
Kokichi Futatsugi abstract
13:50 - 14:30A note on the independence of premiss rule
Hajime Ishihara abstract
14:30 - 15:10 An attempt to systematically produce proof scripts in CafeOBJ CITP from proof scores in CafeOBJ
Kazuhito Ogata abstract
15:10 - 15:30Break
Session 2
15:30 - 16:10Awareness and Predictability
Satoshi Tojo abstract
16:10 - 16:50Completion Revisited (Work in Progress)
Nao Hirokawa abstract
16:50 - 17:00Break
Session 3
17:00 - 17:40Constructive provability of existence statements
Makoto Fujiwara abstract
17:40 - 18:20Overview of logic based tools: symbolic execution for binaries and SMT solver
Mizuhito Ogawa abstract
18:20 - 19:00A (quite) general method to prove non-re for Kripke frames and real-valued based logics
Norbert Preining abstract
19:00 - 21:30Dinner Meeting
Friday, December 04
Session 4
9:30 - 10:10The power of the epsilon calculus
Matthias Baaz
10:10 - 10:40Break
Session 5
10:40 - 11:20Foundations of Logic Programming in Hybridised Logics with User-defined Sharing
Daniel Gaina abstract
11:20 - 12:00Infinite games in the Cantor space and subsystems of second order arithmetic
Takako Nemoto abstract
12:00 - 13:30Lunch Meeting
Session 6
13:30 - 14:10Cut-Elimination Theorem for Expansions of Belnap-Dunn's Four Valued Logic via Functional Weak-Completeness
Katsuhiko Sano abstract
14:10 - 14:50TBD
Yuki Chiba abstract
14:50 - 15:00Closing


Abstracts

Recent Developments on Specification and Verification with CafeOBJ
(by Futatsugi)

Abstract: Recent developments around CafeOBJ proof score method for verifying specification are surveyed. Several developed proof score styles as open-close, spec-calculus, gen&check are explained, and their relationships and future potential is discussed.


A note on the independence of premiss rule
(by Ishihara)

Abstract: We prove that certain theories of (many-sorted) intuitionistic predicate logic is closed under the independence of premiss rule (IPR). As corollaries, we show that HA and HA^omega extended by some non-classical axioms and non-constructive axioms are closed under IPR.


An attempt to systematically produce proof scripts in CafeOBJ CITP from proof scores in CafeOBJ
(by Ogata)

Abstract: Proof scores are proof plans written in an algebraic specification language, such as CafeOBJ. Proof scores can be written as programs and then are flexible but subject to human errors as programs. Constructor-based Inductive Theorem Prover (CITP) has been designed and implemented mainly by Daniel Gaina to exclude human errors. The Gaina's CITP has been implemented in Maude. Based on the Gaina's CITP, Toshimi Sawada, the implementor of CafeOBJ and some others have designed and implemented CITP on CafeOBJ (called CafeOBJ CITP) in Common Lisp. We will discuss an attempt to systematically produce proof scripts in CafeOBJ CITP from proof scores in CafeOBJ.


Awareness and Predictability
(by Tojo)

Abstract: In criminal cases, we need to decide whether the crime is caused intentionally or not. Thus, the judgement is greatly influenced by the predictability of results and the awareness of facts. We have modeled several criminal cases in Dynamic Epistemic Logic (DEL) and Action Model. In this talk, we introduce the concept of awareness into Action Model of multi-agent to reason about the predictability and model the sensitive cases such as the willful negligence. Furthermore, we implement an extended DEMO (Dynamic Epistemic MOdeling), including the awareness in DEL and Action Model, and observe the relation between the judgements of cases and the epistemic states or awareness.


Completion Revisited (Work in Progress)
(by Hirokawa)

Abstract:The Knuth-Bendix completion is a fundamental procedure for proving validity of equalities. In this talk I present a new variant of completion.


Constructive provability of existence statements
(by Fujiwara)

Abstract: Constructive provability is of great interest in foundation of mathematics. We consider (basically) two kinds of constructive provability of existence statements and investigate the relation between them from the viewpoint of formalist foundation. One is from constructive mathematics and the other is from computable and reverse mathematics. In this talk, we overview the recent development of this line of research along with my own work.


Overview of logic based tools: symbolic execution for binaries and SMT solver
(by Ogawa)

Abstract: We overview needs and ideas for dynamic symbolic execution for disassembly of malware, in which a backend engine is an SMT solver for nonlinear (polynomial) constraints. As long as time allows, we will also overview on typical techniques for solving nonlinear constraints.


A (quite) general method to prove non-re for Kripke frames and real-valued based logics
(by Preining)

Abstract: We present a very general method to prove large classes of logics to be non recursively enumerable.


Foundations of Logic Programming in Hybridised Logics with User-defined Sharing
(by Gaina)

Abstract: In this talk we present the foundation of logic programming in hybridised logics. The basic logic programming semantic concepts such as query and solutions, and the fundamental results such as the existence of initial models and Herbrand's theorem, are developed over a very general hybrid logical system. We employ the hybridisation process proposed by Diaconescu over an arbitrary logical system captured as an institution to define the logic programming framework.


Infinite games in the Cantor space and subsystems of second order arithmetic
(by Nemoto)

Abstract: It is known that almost all known subsystems of second order arithmetic is characterized by determinacy of infinite games in the Cantor space. In this talk, I introduce several easy examples of games in the Cantor space and how to characterize subsystems of second order arithmetic.


Cut-Elimination Theorem for Expansions of Belnap-Dunn's Four Valued Logic via Functional Weak-Completeness
(by Sano)

Abstract: This talk concerns a syntactic cut-elimination theorem for expansions of Belnap-Dunn's four-valued logic, whose four values are: true, false, neither (gap), and both (glut). First, I introduce the outline of Belnap-Dunn's four-valued logic regarding Dunn's relational semantics, which specifies when a given formula is *related to* the classical truth values (1 and 0) and also provides us with the more intuitive understanding of a particular connective than semantics based on four-valued tables. Moreover, I review the notion of functional weak-completeness from (Omori and Sano 2015) as a generalization of functional completeness in Belnap-Dunn's four-valued logic and also demonstrate which set of connectives becomes functionally weak-complete. Second, I explain how the idea of Dunn's relational semantics enables us to generate effectively inference rules for a given connective to construct a (G3-style) sequent calculus. Finally, I show that the admissibility of cut in a sequent calculus for *any* set of connectives is reduced constructively to the admissibility of cut in a sequent calculus for a weak-functionally complete set of connectives.


TBD
(by Chiba)

Abstract: TBD

Contact
nao-aoki@jaist.ac.jp