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:30 | A 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:30 | Break |
| Session 2 | |
| 15:30 - 16:10 | Awareness and Predictability Satoshi Tojo abstract |
| 16:10 - 16:50 | Completion Revisited (Work in Progress) Nao Hirokawa abstract |
| 16:50 - 17:00 | Break |
| Session 3 | |
| 17:00 - 17:40 | Constructive provability of existence statements Makoto Fujiwara abstract |
| 17:40 - 18:20 | Overview of logic based tools: symbolic execution for binaries
and SMT solver Mizuhito Ogawa abstract |
| 18:20 - 19:00 | A (quite) general method to prove non-re for Kripke frames and real-valued based logics Norbert Preining abstract |
| 19:00 - 21:30 | Dinner Meeting |
| Friday, December 04 | |
| Session 4 | |
| 9:30 - 10:10 | The power of the epsilon calculus Matthias Baaz |
| 10:10 - 10:40 | Break |
| Session 5 | |
| 10:40 - 11:20 | Foundations of Logic Programming in Hybridised Logics with User-defined Sharing Daniel Gaina abstract |
| 11:20 - 12:00 | Infinite games in the Cantor space and subsystems of second order arithmetic Takako Nemoto abstract |
| 12:00 - 13:30 | Lunch Meeting |
| Session 6 | |
| 13:30 - 14:10 | Cut-Elimination Theorem for Expansions of Belnap-Dunn's Four Valued Logic via Functional Weak-Completeness Katsuhiko Sano abstract |
| 14:10 - 14:50 | TBD Yuki Chiba abstract |
| 14:50 - 15:00 | Closing |
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 |
|---|