Note that this HTML page was
generated from Word 2000. Some
of the code cannot be pasted into Qi. You are advised to download the program
files through the above link. 14 Proof Systems 14.1 Building Automated Theorem Provers_____ We closed the previous chapter
with an examination of the type system of Qi, and we saw that the process of
type checking was actually a process of automated deduction which could be mechanised so a computer could perform type
checking unaided. We also saw that refinement rules enabled us to define types where it was very
difficult to efficiently automate type checking. In this chapter, we will look at some applications of Qi
to automated deduction - the original application area for which the language
was designed. Every automated deduction program can be represented as an attempt to mechanise the
application of refinement rules to enable the automatic proof of theorems. Such programs vary from systems that require human
guidance at every step of the proof (called proof checkers) to fully automated theorem-provers (ATPs) that require little or no human guidance at
all. In between is a large class of ATPs that are capable of performing some steps
automatically, but may require human guidance from time to time. These programs have been written in
many languages, including C, Prolog, Lisp and SML. Some have proved difficult
theorems in mathematics and logic. But is it justified to accept the verdict
of a computer? Suppose we have
encoded an ATP in 10,000 lines of C. What guarantee is there that this ATP is
correct? How can we sure that the formulae that the ATP says are theorems are really theorems? It is almost impossible to write a C
program over 1,000 lines that does not contain significant errors, and an ATP
of 10,000 lines of C is almost certain not to work properly unless it has
been debugged and tested over several man-years. This is the reliability problem in building
ATPs; we have a set of refinement rules and we have a theorem-prover; but how do we know that the
program faithfully encodes what is in the refinement rules? To put the matter
formally, suppose D |- F A holds when A follows from a set
of formulae D by the
refinement rules of F. Suppose der(D, A) holds when our theorem-prover T
for F says “proved” (or some equivalent verdict). How do we know that der(D, A) implies D |- F A? In other words, how do we know T is sound in the sense
of chapter 7? One way of increasing certainty is
to write T so that the only operations that build up proofs are those
operations that apply refinement rules of F. So as long as we have correctly represented the
refinement rules of F, T should be sound. Qi was originally designed to facilitate the high-level
specification of ATPs, and working in Qi, this encoding of refinement rules
is very easy. We just write them to Qi and Qi compiler will compile these refinement
rules to machine code, removing the need for us to write our own routines for
manipulating the proof. But working at the level of
refinement rules is extremely tedious. The system is a proof checker,
nothing more. Difficult proofs require large numbers of steps. But not every
proof-building operation need be so low-level as the application of a single
refinement rule. An operation in T may be defined in terms of many
applications of refinement rules; there is no need to work at the lowest
possible level. As an analogy, consider the way in
which computers are programmed. Every computer has a machine code instruction
set within which all instructions to it are translated. Despite its very low level, that
instruction set will support high-level mainstream computer languages like C++ and Prolog. Each high-level language is supported by a compiler from native source into the
resident machine code instruction set.
For ATPs, our machine code instruction set is the set whose elements
apply one refinement rule. Our goal is to evolve a high-level proof language for calling
up these primitive operations, so that long proofs can be executed in a few
steps rather than many. In this
chapter, we will see how to build such proof languages in Qi. We begin with a look at proof
systems. 14.2 Proof Systems_________________________ A proof system is a notation
devised for representing reasoning. There are many different kinds of proof system; but they all share a
common cluster of features. 1. A proof system L has syntax rules: these are rules of
formation that determine when an expression is a formula of that proof system
and when it does not. For
example, thinking of arithmetic
as a proof system, the expression
1 + 2 - (4 * 5) is a formula; but * 6 * -78 + + - 7 is not. Formulae of a
proof system that meet the requirements of its syntax are called well-formed
formulae of L or wffs for short. 2. A proof system L has a proof
theory. A proof theory defines the provability relation, usually by giving refinement rules for proving sequents. If A is provable from a set D of wffs of L then we write D |- L A. If D is empty then A is a theorem of L, written
|- L A. 3. A proof system has a semantics. A
semantics gives rules for assigning interpretations to wffs. When the symbols of a wff A are given meaning in
accordance with the semantics, we say A has been given an interpretation
I. When a wff A is true
under I then I is a model of A,
written I |= L A. If A is false under I then I is a countermodel of the
wff. When every interpretation
of A is a model then A is valid, written |= L A. A proof system in which every theorem is valid is referred to as sound. A proof system in which every valid wff is a
theorem is complete. If a proof system is both sound and complete then its
semantics is said to characterise that
proof system. For example, we may interpret a,
b, c in a + b = c as denoting 1,2 and 3
respectively, but not Tom, Dick and Harry. The semantics of algebra forbids this sort of interpretation. The interpretation that assigns a
in a = a * a the value 1 is a model since 1 = 1 * 1 is true. However a = a * a
is not valid in algebra since the interpretation that assigns a
the value 2 is a countermodel, since 2 = 2 * 2 is false. a
* b = b * a, on the other hand, is obviously valid. 4. A proof system may have a heuristics; or a set of principles to help people (or
computers) reason with it. For
example, in algebra we have a principle that tells us to isolate all
occurrences of an unknown on one side of an equation. This is part of the heuristics
of algebra. 5. The symbols of any proof system
partition into a set of logical constants and a set of logical
variables. For
example in algebra, the constants are the +, -, * and / and the
variables a, b, c etc. Two wffs are variants of each
other if they can be derived from each other by the uniform substitutions of
the logical variables within them. An important principle we will call the variant
principle states.
The Variant
Principle If |- L
A, and B is a variant of A, then |- L B. So given a * b = b
* a is a theorem of algebra, so is a * c = c * a,
(a - b) * c = c * (a - b) etc. 14.3 Propositional Calculus__________________ One familiar proof system is propositional
calculus (PC), which
captures some basic patterns of inference involving the connectives &
(and), v (or), ~ (not), ® (if ... then
...), and « (if and only if). These elements are the logical constants of the propositional calculus. As well as these connectives there
is an unlimited supply of propositional variables p, q, r, s, p', q',
r', s'.... . These propositional variables can be
made to stand for sentences. Thus identifying p with the sentence "Logic is easy." and q with
the sentence "Students like logic." determines the meaning of all
propositional wffs containing only p and q as
variables (figure 14.1). Wff
Interpretation (p ® q)
If logic is easy then students like logic. (p v q)
Either logic is easy or students like logic. ((~ p) v q)
Either logic is not easy or students like logic. ((~ p) & (~ q)) Logic
is not easy and students do not like logic. (p « q)
Logic is easy if and only if students like logic. Figure 14.1 A
reading of some propositional calculus wffs The syntax |