This project originated from an idea by Tor Sandqvist from Uppsala. It is concerned with a uniform theorem prover for first order logic and is based on the observation that any formula can be written using only the NAND operator.
e.g. in the following notation for a NAND formula,
[a,b,c] means "it is not the case that a & b & c". Then, for propositional formulas:
a = [[a]]; a&b = [[a,b]]; a or b = [[a][b]]; a -> b = [a[b]], etc.
Any proper sub-formula of the form [[x]] can be simplified to x.
Thus [[[a]],[b]] simplifies to [a[b]] and [[[[a]],[b]]] simplifies to [[a,[b]]] and [[[[a],[b]]]] simplifies to [[a]],[b]].
Quantified formulas can also be written in a similar form as can be explained later on in the project if necessary.
The first part of the project is to produce a translator that, given a formula in propositional logic, produces an equivalent simplified NAND formula.
The second part is to write a theorem prover for developing proof trees according to the extension and closure rules given below and to consider various ways of selecting which formula to use in the extension rule. The prover should be tested on problems from the database TPTP (Thousands of Problems for Theorem Provers).
The third part is to investigate new reduction steps, which maintain equivalence, and in some cases can avoid the need for using the extension rule at all.
One possible notation for NAND formulas is the one used above, that makes use of Prolog lists. Two special cases of a NAND formula should be mentioned: [ ] represents "~ empty conjunction", which is equivalent to ~True by convention and hence to False, and [[ ]] represents "~~True", which is equivalent to True.
If [[ ]] occurs within some other NAND formula it can be removed. There are other kinds of simplification (other than removing double brackets), which you can investigate in Part 3 of the project. e.g. if [ ] appears in a NAND formula f - as in f = [x1, [ ], ...], which is equivalent to "~(x1 & False & ...)", or to ~False - the whole formula f is equivalent to [[ ]] (i.e. to True). If f is itself embedded in some other NAND formula h, then f can simply be removed from h. e.g. h = [y,f,z] simplifies to h=[y,z].
From now on, formula will mean NAND-formula. Also, xi is called a constituent of a formula [x1,...,xn].
Given a propositional formula f, we would like to show if it is valid, or not. This is done by constructing a "NAND-proof tree" (henceforth shortened to NPT). The root node of an NPT is labelled by the formula f and is open. There is one extension rule (E) and two branch closure rules (CL) and (CA). Each node n will be labelled by a formula g (sometimes expressed as "g at n").If f is at a leaf in open branch B and f appears as a constituent of some formula g at a node in B the branch becomes closed.
If f is at a node in open branch B and f is a constituent of the formula at the leaf of B the branch becomes closed.
If a formula g = [x1,...,xm] is a constituent of a formula at some node in B, then expand the tree by appending m+1 new leaves to B, such that the first leaf is labelled by g and the other m leaves are labelled by the xi, 1<=i<=m. (Note: if g=[ ] there is one new leaf labelled by g.) The first branch can be closed by rule CL. The remaining branches are still open.
If all branches in a tree are closed then the tree is closed. Otherwise, the tree is open. An example of a closed tree for the formula [[q,[p]], [p], q,[r]], equivalent to (q -> p) -> (p or (q -> r)), is shown below left. On the other hand, if construction of a tree reaches a situation when no more rules can be applied and the tree is open, then an assignment that falsifies the initial formula can be found as follows. Let B be a branch that is open. Each atom that labels a node is assigned false. Each atom that is a constituent of a formula at a node in B is assigned true. Any atoms still unassigned can be assigned true or false. An example of an open tree is shown below right. The assignments obtained from the two open branches are, respectively, {b=false, a=true } and {c=false, d=false, a=true}, both of which falsify the root formula [a,[b,[[c],[d]]]], which is equivalent to a ->(b & (c or d)).
If time the prover could be extended to first order logic. Some helpful hints will be given to any group that chooses this project.