Automated Reasoning with Analytic Tableaux and Related Methods
This book constitutes the refereed proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2003, held in Rome, Italy in September 2003. The 20 revised full papers presented were carefully rev
- PDF / 2,764,781 Bytes
- 283 Pages / 430 x 660 pts Page_size
- 66 Downloads / 233 Views
Noncommutative Logic (NL) has been introduced by Abrusci and Ruet (NonCommutative Logic I, Annals of Mathematical Logic, 2001). NL is a refinement of Linear Logic (LL) and a conservative extension of Lambek Calculus (LC). Therefore, NL is a constructive logic (i.e. proofs are programs). Noncommutative logic allows to deal with commutative and non-commutative conjunctions and disjunctions. In Noncommutative Logic sequents are order varieties on finite sets of occurrences of formulas. The talk surveys the main results obtained in Noncommutative logic in 20012003, by several authors: 1. 2. 3. 4. 5. 6.
proof-nets, sequent calculus, and sequentialization theorem, proof search, phase semantics, and completeness theorem, reduction of proof-nets, and semantics of proofs, modules.
M. Cialdea Mayer and F. Pirri (Eds.): TABLEAUX 2003, LNAI 2796, p. 1, 2003. c Springer-Verlag Berlin Heidelberg 2003
Dynamical Method in Algebra: A Survey (Abstract) Thierry Coquand Computing Science Department G¨ oteborg University, Sweden [email protected]
The system D5, of J. Della Dora, C. Dicrescenzo, and D. Duval, allows computations in the algebraic closure of a field, though it is known that such a closure may fail to exist constructively. This mystery has been recently analysed in the work of Coste-Lombardi-Roy. A survey of this work and its connections with the system D5 is presented in this talk. In particular I present in detail the notion of “geometric logic” which allows a quite suggestive notion of proofs which may be of independent interest.
M. Cialdea Mayer and F. Pirri (Eds.): TABLEAUX 2003, LNAI 2796, p. 2, 2003. c Springer-Verlag Berlin Heidelberg 2003
Automated Theorem Proving in Generation, Verification, and Certification of Safety Critical Code (Abstract) Johann Schumann RIACS / NASA Ames Moffett Field, CA 94035 [email protected]
With increased complexity of missions, the need for high quality, mission- and safety-critical software has increased dramatically over the past few years. Several incidents (e.g., Mars Polar Lander) have shown that software errors can cause total loss of a mission. Together with tight budgets and schedules, software development and certification has become a serious bottleneck. In this talk, I report on work done in the Automated Software Engineering group at NASA Ames. We are developing automatic program synthesis systems for state estimation and navigation, AutoFilter, and data analysis (AutoBayes). These tools automatically generate documented C/C++ code from compact, high-level specifications. For safety-critical applications, the generated code must be certified, since the alternative of verifying the code generator is not feasible. We support the certification process by combining code certification with automatic program synthesis. Code certification is a lightweight approach for formally demonstrating important aspects of software quality. Its basic idea is to require the code producer to provide formal proofs that the code satisfies certain safety properties. These proofs serv
Data Loading...
