DPL | |
Description | This
dissertation introduces denotational proof languages (DPLs). DPLs can be
used to express and check (validate) formal proofs. DPL proofs are typically
readable, writable, compact, and easy to check. Syntactically, DPL proofs
are generated by context-free grammars in such a way that the text of the
proof reflects its logical structure. Semantically, the formal meaning of
a DPL proof is specified relative to a given assumption base, which is a
set of premises, i.e., a set of propositions that we take for granted for
the purposes of the proof. The key idea is that if a DPL proof is sound,
then its meaning (denotation) is the conclusion established by the proof;
if the proof is unsound, then its meaning is error. To obtain that meaning,
we evaluate the proof in accordance with the formal semantics of the language.
Evaluation will either produce the advertised conclusion, which will verify
that the proof is sound, or else it will generate an error, which will indicate
that the proof is unsound. Thus in DPLs evaluation is tantamount to proof
checking. We illustrate the core ideas by introducing CN D, a simple DPL for classical firstorder logic with equality. We develop the theory of CN D in detail, prove its soundness and completeness, present dozens of sample proofs, and develop a number of proof optimization procedures that remove redundancies and unnecessary "detours". We also discuss CN D as a formal analysis of the concept of deduction, and compare it with previous formalizations such as Hilbert calculi, sequent systems, and proof trees. We then introduce the *u-calculus, a terse formal system that can be viewed as a unifying framework for DPLs, much as the *-calculus can be seen as a unifying formal framework for functional programming languages. The *u-calculus allows for proof abstraction via methods. Methods are to proofs what procedures are to computations. They are essential for task decomposition and complexity management in proof engineering. Methods are made possible by a careful integration of computation and deduction: the *u-calculus can be used both for programming and for proofs. More interestingly, we show how methods, when combined with recursion, pattern matching, etc., can be used for proof search and theorem proving. We work out the rudiments of the theory and metatheory of the *u-calculus, and present several examples of *u systems. |
Deliverables | Athena, dissertation |
Contributions | DPL proofs are typically readable, writable, compact, and easy to check. |
Researchers | Kostas Arkoudas |
Language | ML |
Subprojects | subprojects |