The research for this thesis has followed two main paths: the one of probability logics and the other of type systems and logical frameworks, bringing them together through interactive theorem proving. With the development of computer technology and the need to capture real-world dynamics, situations, and problems, reasoning under uncertainty has become one of the more important research topics of today, and one of the tools for formalizing this kind of knowledge are probability logics. Given that probability logics, serving as decision-making or decision-support systems, often form a basis for expert systems that find their application in fields such as game theory or medicine, their correct functioning is of great importance, and formal verification of their properties would add an additional level of security to the design process. On the other hand, in the field of logical frameworks and interactive theorem proving, attention has been directed towards a more natural way of encoding formal systems where derivation rules are subject to side conditions which are either rather difficult or impossible to encode naively, in the Edinburgh Logical Framework \LF or any other type-theory based Logical Framework, due to their inherent limitations, or to the fact that the formal systems in question need to access the derivation context, or the structure of the derivation itself, or other structures and mechanisms not available at the object level. The first part of the thesis deals with the development and formal verification of probability logics. First, we introduce a Probability Logic with Conditional Operators - LPCP, its syntax, semantics, and a sound and strongly-complete axiomatic system, featuring an infinitary inference rule. We prove the obtained formalism decidable, and extend it so as to represent evidence, making it the first propositional axiomatization of reasoning about evidence. Next, we show how to encode probability logics LQI and LQnI in the Proof Assistant Coq. Both of these logics extend classical logic with modal-like probability operators, and both feature an infinitary inference rule. LQI allows iterations of probability operators, while LQnI does not. We proceed to formally verify their key properties - soundness, strong completeness, and non-compactness. In this way, we formally justify the use of probabilistic SAT-solvers for the checking of consistency-related questions. In the second part of the thesis, we present LFP - a Logical Framework with External Predicates, by introducing a mechanism for locking and unlocking types and terms into LF, allowing the use of external oracles. We prove that LFP satisfies all of the main meta-theoretical properties (strong normalization, confluence, subject reduction, decidability of type checking). We develop a corresponding canonical framework, allowing for easy proofs of encoding adequacy. We provide a number of encodings - the simple untyped lambda-calculus with a Call-by-Value reduction strategy, the Design-by-Contract paradigm, a small imperative language with Hoare Logic, Modal Logics in Hilbert and Natural Deduction style, and Non-Commutative Linear Logic (encoded for the first time in an LF-like framework), illustrating that in LFP we can encode side-conditions on the application of rules elegantly, and achieve a separation between derivation and computation, resulting in cleaner and more readable proofs. We believe that the results presented in this thesis can serve as a foundation for fruitful future research. On the one hand, the obtained formal correctness proofs add an additional level of security when it comes to the construction of expert systems constructed using the verified logics, and pave way for further formal verification of other probability logics. On the other hand, there is room for further improvement, extensions, and deeper analysis of the LFP framework, as well as the building of a prototype interactive theorem prover based on LFP and discovering its place in the world of proof assistants.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00911517 |
| Date | 15 October 2013 |
| Creators | Maksimovic, Petar |
| Publisher | Université Nice Sophia Antipolis |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | English |
| Type | PhD thesis |
Page generated in 0.0019 seconds