This webpage describes an initial proof checker for axiomatic language. For background see this axiomtic language overview or this webpage on proof. This proof checker is defined for and is written in a restricted form of axiomatic language called SAL - Simplified Axiomatic Language. Queries in SAL give the steps of a proof and their successful execution confirms that the proof is correct. The sections below give an overview of the system. Future work will add some inference rules to handle proof-by-contradiction.

In regular axiomatic language, called General Axiomatic Language - GAL, string variables can occur anywhere within a sequence. This enables one-line definitions of some common list predicates:

(member %x ($1 %x $2)). (concat ($1) ($2) ($1 $2)). (append1 ($) %x ($ %x)). ! append one expr to end of sequenceExample valid expressions generated by these axioms include (member %x ($1 %x $2)), (member %x ($1a %1 $1b %x $2a $2b), and (append1 ($1 % $2) %x ($1 % $2 %x)). But unification with unrestricted string variables can have multiple most-general solutions, such as unifying ($ a) with (a $) or unifying ($1 $) with ($ $2). In SAL - Simplified Axiomatic Language, we restrict string variables to the ends of sequences. The above list predicates would be defined by the following SAL axioms:

(member %x (%x $)). (member %x (% $))< (member %x ($)). (concat () ($) ($)). (concat (% $1) %2 (% $12))< (concat ($1) %2 ($12)). (append1 () %x (%x)). (append1 (% $) %x (% $'))< (append1 ($) %x ($')).Valid expressions for these SAL axioms include (member %x (%1 %2 %x $)), (concat (%1 %2 %3) ($2) (%1 %2 %3 $2)), and (append1 (%1 %2) %x (%1 %2 %x)). Note that in SAL expressions, string variables are analogous to list tail variables in Prolog:

SAL Prolog (a %X $Z) [a, X | Z]In SAL, unification has a single most-general result, or it fails. This means we can have a Prolog-like top-down resolution solver for SAL predicates, which is what has been done for this proof checker. Note that this is *not* an implementation of (GAL) axiomatic language, which requires automatic transformation of high-level specifications. For example, higher-order forms in SAL axioms can easily lead to non-termination of the solver. Axioms for a program in SAL must be carefully written to achieve efficiency.

For internal processing of axiomatic language, it is possible to get even simpler. In PAL - Primitive Axiomatic Language, sequences are replaced by pairs and there are no string variables. The PAL definition of the member predicate is as follows:

(` (`member (%x ((` (%x %$)) `)))). (` (`member (%x ((` (% %$)) `))))< (` (`member (%x ((` %$) `)))).(Here we use an atom for the predicate name to avoid the complexity of syntax extension symbols. Note our use of the atom ` when representing SAL sequences in PAL.) PAL is used for data representation and processing inside the proof checker.

In order to write axioms and valid clauses that must be processed as data, we need an encoding. (To process variables, for example, they can't be real variables. They must be ground expressions.) The syntax extensions of axiomatic language are helpful here. We let atoms, variables, and syntax extension symbols be represented by syntax extension symbols with a prepended underscore:

actual tokens encoded tokens `x _`x -- atoms %a _%a -- expression vars $1 _$1 -- string vars abc _abc -- syntax extension symbolsAn encoded axiom/clause is just a sequence of its encoded conclusion and condition expressions. An encoding of the axioms for natural numbers (with atoms for the zero and successor symbols) is as follows:

((_num _`0)) ((_num (_`s _%)) (_num _%))

A proof is defined in a "check" predicate which is then executed as an SAL query. A successful query solution indicates that the proof is correct. The format of the check predicate is informally sketched as follows:

(check (.. (#lbl# #ax#)..) - labeled encoded SAL axioms in "original" set -- all valid clauses are proved wrt to these original axioms -- this original ax set has the ax set name _ (underscore) (..#chk_step#..) - sequence of "check steps" -- these steps prove new valid clauses and equivalent axiom sets (..(#lbl# #axlblseq#)..) - output list of equivalent axiom sets -- we list each axiom set name label and the labels of its axioms (..(#lbl# #vcP#)..) - output list of labeled valid clauses as PAL -- (Note that valid clauses in PAL form are not very readable!) ) #chk_step# = (#lbl# #clause to prove# ..infer_proof..) | (#lbl# #clause to prove# ..induc_proof..) | (_axset #new ax set label# #lbls of axioms in new ax set# -- axioms in new ax set must already be proved valid wrt original ax set ..(#orig ax lbl# #orig ax# ..proof..).. -- each orig axiom not in the new set must be prove valid wrt new ax set ) ..infer_proof.. = #vc_lbl# {#cond# #vc_lbl# | #cond_perm/add#} #vc_lbl# = label of an existing valid clause (axiom or previously proved) -- The first #vc_lbl# initializes the "current valid clause". Each subsequent infer_proof step modifies this clause. #cond# = decimal symbol index of a current valid clause condition (1 .. n) -- This condition is unfolded against the conclusion of the next #vc_lbl#, which produces a new current valid clause. #cond_perm/add# = sequence of permuted decimal condition numbers with an optional _ underscore inserted for each added condition at that position. The modified clause becomes the new current valid clause. This inference proof step implements the inference rules that a permutation of the conditions of a valid clause gives a valid clause and that adding conditions to a valid clause gives a valid clause. -- At the end of the infer_proof we check that the #clause to prove# is an instance of the current valid clause. ..induc_proof.. = _induc #cond# #axsetlbl# ..(#lblprefix_axlbl# #resulting clause to prove# ..proof..).. -- An induction proof step begins with the keyword '_induc'. We unfold the #cond# condition of the #clause to prove# against the specified set of axioms #axsetlbl# (which would be _ to unfold against the original axiom set). For each successful unfold, the resulting clause is given and has a label with an arbitrary prefix followed by the label of the axiom that produced that resulting clause. A proof of this resulting clause is given, which may be an inference proof or another induction proof. For an unfold step in an inference proof, we may unfold against the #clause to prove# in addition to already proved valid clauses.

This section gives example proofs that are actual executions of the check predicate using the SAL query solver. Double-hyphen -- comments have been inserted into the query solver output to add to the axiomatic language comments that start with !. We use single letter predicate names n,p below in place of longer symbol names num,plus for conciseness.

These examples give the labeled axioms n0,n1 for natural numbers:

n0 (`n `0). ! zero is a natural number n1 (`n (`s %))< (`n %). ! if n is a nat num, so is succ(n)Here we use atoms for all symbols to make the final valid clause PAL output more consise. These axioms n0,n1 are our initial valid expressions. Replacing the variable in n1 with the atom `x gives valid clause nx, an instance of n1:

nx (`n (`s `x))< (`n `x). ! an instance of n1, so nx is validUnfolding valid clause n1's condition 1 with itself gives this valid clause n2:

n2 (`n (`s (`s %)))< (`n %). ! if n is num, then so is n+2The complete query and its output shows these two inference proofs:

%lvcP < ! final set of valid clauses is displayed as query output (check ( ! labeled axioms for natural numbers: (n0 ((_`n _`0))) ! 0 is a natural number (n1 ((_`n (_`s _%)) (_`n _%))) ! if n is nat num, n+1 is nat num ) ! - note atoms for set predicate name and zero, successor symbols ! (leading _ means atoms and vars represented by syntax extension symbols ( ! some simple valid clause inference proof steps to be checked: (nx ((_`n (_`s _`x)) (_`n _`x)) n1) ! - clause nx is just an instance of axiom n1 (n2 ((_`n (_`s (_`s _%))) (_`n _%)) n1 1 n1) ! if n is nat num, so is n+2 ! - n2 is proved by unfolding n1 (cond 1) with itself ) %laxsl %lvcP). SOLUTIONS: ((n0 (((atom ()) ((atom "n") ((atom "0") (atom ())))))) (n1 (((atom ()) (( atom "n") (((atom ()) ((atom "s") ((var "%") (atom ())))) (atom ())))) (( atom ()) ((atom "n") ((var "%") (atom ())))))) (nx (((atom ()) ((atom "n") (((atom ()) ((atom "s") ((atom "x") (atom ())))) (atom ())))) ((atom ()) (( atom "n") ((atom "x") (atom ())))))) (n2 (((atom ()) ((atom "n") (((atom () ) ((atom "s") (((atom ()) ((atom "s") ((var "%") (atom ())))) (atom ())))) (atom ())))) ((atom ()) ((atom "n") ((var "%") (atom ()))))))) -- the output shows the internal PAL representation for the valid clauses n0,n1,nx,n2 time, #solns: 0.06 1 -- execution time was .06 seconds, with just one query solution found -- failure to get a solution would mean an error in the proof! max stack size, max solve fn depth, # occur chks: 175257 5955 81329 -- these internal calculation parameters can be ignoredNote that the binary-tree PAL output with all its nested parentheses is pretty much unreadable, but a user of this proof checker would really need to deal with only encoded SAL input.

This next example uses single-letter syntax extension symbols n,0,s, which results in a much more voluminous valid clause PAL output, since the bit atoms for the different characters are displayed. In this example, our inference proof unfolds n1 condition 1 with itself to produce n2 as the "current valid clause", which then has its condition 1 unfolded with valid clause n0 to produce the unconditional valid clause n2ve = (n (s (s 0)))., which generates the valid expression (n (s (s 0))), or "two is a natural number".

(%laxsl %lvcP) < (check ( ! labeled axioms for natural numbers: (n0 ((_n _0))) ! 0 is a natural number (n1 ((_n (_s _%)) (_n _%))) ! if n is nat num, n+1 is nat num ) ( ! a simple valid clause inference proof to be checked: (n2ve ((_n (_s (_s _0)))) n1 1 n1 1 n0) ! 2 is a nat num ! - Successive unfolds can produce unconditional valid clauses ! representing valid expressions. ) %laxsl %lvcP). SOLUTIONS: (((_ (n0 n1))) ((n0 (((atom ()) (((atom ()) ((atom ()) (((atom ()) (((atom () ) ((atom "char") (((atom ()) ((atom "0") ((atom "1") ((atom "1") ((atom "0" ) ((atom "1") ((atom "1") ((atom "1") ((atom "0") (atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) (((atom ()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom "0") ((atom "0") ((atom "1") ((atom "1") ((atom "0") ((atom "0") ((atom "0") ((atom "0") (atom ())))))))))) ( atom ())))) (atom ()))) (atom ())))) (atom ())))))) (n1 (((atom ()) (((atom ()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom "0") ((atom "1") ((atom "1") ((atom "0") ((atom "1") ((atom "1") ((atom "1" ) ((atom "0") (atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) ((( atom ()) (((atom ()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") ((( atom ()) ((atom "0") ((atom "1") ((atom "1") ((atom "1") ((atom "0") ((atom "0") ((atom "1") ((atom "1") (atom ())))))))))) (atom ())))) (atom ()))) ( atom ())))) ((var "%") (atom ())))) (atom ())))) ((atom ()) (((atom ()) (( atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom "0") (( atom "1") ((atom "1") ((atom "0") ((atom "1") ((atom "1") ((atom "1") (( atom "0") (atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) ((var "%") (atom ())))))) (n2ve (((atom ()) (((atom ()) ((atom ()) (((atom ()) (( (atom ()) ((atom "char") (((atom ()) ((atom "0") ((atom "1") ((atom "1") (( atom "0") ((atom "1") ((atom "1") ((atom "1") ((atom "0") (atom ()))))))))) ) (atom ())))) (atom ()))) (atom ())))) (((atom ()) (((atom ()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom "0") ((atom "1") ((atom "1") ((atom "1") ((atom "0") ((atom "0") ((atom "1") ((atom "1") ( atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) (((atom ()) (((atom ()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom "0") ((atom "1") ((atom "1") ((atom "1") ((atom "0") ((atom "0") ((atom "1" ) ((atom "1") (atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) ((( atom ()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) (( atom "0") ((atom "0") ((atom "1") ((atom "1") ((atom "0") ((atom "0") (( atom "0") ((atom "0") (atom ())))))))))) (atom ())))) (atom ()))) (atom ()) ))) (atom ())))) (atom ())))) (atom ())))))))) -- The initial output gives the list of "equivalent" axiom sets. In this case we just have the original axiom set, which has label _ and contains axioms n0 n1. -- After the equivalent axiom sets list we have the dump of PAL valid clauses n0,n1,n2ve, which includes the bit atoms of the symbol characters. time, #solns: 0.50 1 max stack size, max solve fn depth, # occur chks: 404750 14282 1793667

These examples give axioms for "q-numbers", where a q-number is just a natural number with predicate name "q". Given natural number axioms n0,n1, q-numbers can be defined by this added qn axiom,

qn (q %)< (n %). ! every nat num is a q-numor by these alternative axioms q0,q1:

q0 (q 0). ! zero is a q-number q1 (q (s %))< (q %). ! if n is a q-num, so is n+1This first example proof below starts with original axiom set _ = n0,n1,qn, then proves that q0,q1 are valid clauses wrt axiom set n0,n1,qn, and then in the _axset definition step shows that original axiom qn is a valid clause wrt alternative axiom set NQ = n0,n1,q0,q1, which makes axiom sets _ and NQ equivalent. Note the induction proofs!

(%laxsl %vclbls) < -- we output just vc labels instead of entire clauses (check ( ! axioms for natural numbers and "q" numbers: (n0 ((_n _0))) ! 0 is a natural number (n1 ((_n (_s _%)) (_n _%))) ! if n is nat num, n+1 is nat num (qn ((_q _%) (_n _%))) ! every nat num is a "q-num" ) ! - original axioms n0,n1,qn have ax set label _ ( ! some simple valid clause proof steps to be checked: (q0 ((_q _0)) qn 1 n0) ! q0 derives from qn unfolded with n0 (q1 ((_q (_s _%)) (_q _%)) _induc 1 _ ! unfold against orig ax set n0,n1,qn (q1_qn ((_q (_s _%)) (_n _%)) qn 1 n1) ! - q1 is proved by induction of its cond 1 against axiom qn ) ! (the resulting clause q1_qn is shown valid by unfolding qn with n1) -- The label suffix _qn shows that this clause is the result of unfolding with original ax set axiom qn. (_axset NQ (n0 n1 q0 q1) ! define equivalent ax set (qn ((_q _%) (_n _%)) _induc 1 NQ ! induction on new ax set n0,n1,q0,q1 (qn_n0 ((_q _0)) q0) ! = valid clause q0 (qn_n1 ((_q (_s _%)) (_n _%)) q1 1 qn) ! = unfold q1 with induc hyp qn ! - Note we can unfold valid clause q1 against induction hypothesis qn ! to prove qn! ) ) ! thus ax set n0,n1,qn is valid wrt new ax set n0,n1,q0,q1 -- and thus the two axiom sets are equivalent! ) %laxsl %lvcP), (transpose %lvcP (%vclbls %vcP)). -- transpose step separates the vc labels! SOLUTIONS: (((_ (n0 n1 qn)) (NQ (n0 n1 q0 q1))) (n0 n1 qn q0 q1)) -- our list of equivalent axiom sets shows both sets: _ and NQ -- following that are the labels for all the valid clauses, which are valid with respect to both (equivalent) axiom sets time, #solns: 4.52 1 max stack size, max solve fn depth, # occur chks: 1016492 36992 3509808

This next example proves the q-num axiom sets equivalent, but in the other direction. That is, we start with original axioms n0,n1,q0,q1 and then show that alternative axiom set n0,n1,qn is equivalent.

(%laxsl %vclbls) < (check ( ! axioms for natural numbers and "q" numbers: (n0 ((_n _0))) ! 0 is a natural number (n1 ((_n (_s _%)) (_n _%))) ! if n is nat num, n+1 is nat num (q0 ((_q _0))) ! 0 is a q-num (q1 ((_q (_s _%)) (_q _%))) ! if n is a q-num, n+1 is q-num ) ( (qn ((_q _%) (_n _%)) _induc 1 _ ! induction on orig ax set n0,n1,q0,q1 (qn_n0 ((_q _0)) q0) ! = valid clause q0 (qn_n1 ((_q (_s _%)) (_n _%)) q1 1 qn) ! = unfold of q1 with induc hyp qn ! - Note that we can unfold valid clause against induction hypothesis qn ! to prove qn! ) (_axset QN (n0 n1 qn) ! define equiv ax set (q0 ((_q _0)) qn 1 n0) (q1 ((_q (_s _%)) (_q _%)) _induc 1 QN (q1_qn ((_q (_s _%)) (_n _%)) qn 1 n1) ) ) ) %laxsl %lvcP), (transpose %lvcP (%vclbls %vcP)). SOLUTIONS: (((_ (n0 n1 q0 q1)) (QN (n0 n1 qn))) (n0 n1 q0 q1 qn)) time, #solns: 4.54 1 max stack size, max solve fn depth, # occur chks: 1093990 40023 3491281

Natural number addition (the "plus" function) can be defined by the following axioms, in addition to n0,n1:

p0 (p 0 % %)< (n %). ! 0 plus n = n p1 (p (s %1) %2 (s %3)< (p %1 %2 %3). ! n1 + n2 = n3 => n1+1 + n2 = n3+1These axioms do induction on the first argument. An alternative definition of plus would be axioms n0,n1,pa0,pa1, which do induction on the second argument:

pa0 (p % 0 %)< (n %). ! n plus 0 = n pa1 (p %1 (s %2) (s %3)< (p %1 %2 %3). ! n1 + n2 = n3 => n1 + n2+1 = n3+1This example proves that these two axiom sets are equivalent:

(%laxsl %vclbls) < (check ( ! axioms for natural numbers and their addition: (n0 ((_n _0))) (n1 ((_n (_s _%)) (_n _%))) (p0 ((_p _0 _% _%) (_n _%))) ! (induction on 1st arg) (p1 ((_p (_s _%1) _%2 (_s _%3)) (_p _%1 _%2 _%3))) ) ( ! prove clauses pa0,pa1 valid wrt n0,n1,p0,p1: (pa0 ((_p _% _0 _%) (_n _%)) _induc 1 _ (pa0_n0 ((_p _0 _0 _0)) p0 1 n0) (pa0_n1 ((_p (_s _%) _0 (_s _%)) (_n _%)) p1 1 pa0) ) (pa1 ((_p _%1 (_s _%2) (_s _%3)) (_p _%1 _%2 _%3)) _induc 1 _ (pa1_p0 ((_p _0 (_s _%) (_s _%)) (_n _%)) p0 1 n1) (pa1_p1 ((_p (_s _%1) (_s _%2) (_s (_s _%3))) (_p _%1 _%2 _%3)) p1 1 pa1) ) (_axset PA (n0 n1 pa0 pa1) ! define equiv ax set ! prove original axioms p0,p1 valid wrt alternate axiom set PA (p0 ((_p _0 _% _%) (_n _%)) _induc 1 PA (p0_n0 ((_p _0 _0 _0)) pa0 1 n0) (p0_n1 ((_p _0 (_s _%) (_s _%)) (_n _%)) pa1 1 p0) ) (p1 ((_p (_s _%1) _%2 (_s _%3)) (_p _%1 _%2 _%3)) _induc 1 PA (p1_pa0 ((_p (_s _%) _0 (_s _%)) (_n _%)) pa0 1 n1) (p1_pa1 ((_p (_s _%1) (_s _%2) (_s (_s _%3))) (_p _%1 _%2 _%3)) pa1 1 p1) ) ) ) %laxsl %lvcP), (transpose %lvcP (%vclbls %vcP)). SOLUTIONS: (((_ (n0 n1 p0 p1)) (PA (n0 n1 pa0 pa1))) (n0 n1 p0 p1 pa0 pa1)) time, #solns: 10.42 1 max stack size, max solve fn depth, # occur chks: 3177582 115468 18227102

To express commutativity of addition we need the following utility predicate that asserts that two expressions are identical:

id (== % %). ! relation arguments are identicalWe prove below this valid clause that asserts that if two expressions are identical then their "successors" are identical:

ids (== (s %a) (s %b))< (== %a %b).The commutativity of addition is expressed by proving the following clause valid:

com (== %3a %3b)< (p %1 %2 %3a), (p %2 %1 %3b).In order for this clause to be valid, the two additions, which have their arguments in opposite order, must always give identical results for all argument %1,%2 values.

Our commutativity proof below starts with original axiom set n0,n1,p0,p1,id, then defines and proves equivalent axiom set n0,n1,pa0,pa1,id, then proves the id "successor" valid clause, and finally proves the commutativity valid clause.

! Proof of commutativity! Addition_is_Commutative < (check ( ! axioms for natural numbers and their addition: (n0 ((_n _0))) (n1 ((_n (_s _%)) (_n _%))) (p0 ((_p _0 _% _%) (_n _%))) (p1 ((_p (_s _%1) _%2 (_s _%3)) (_p _%1 _%2 _%3))) (id ((_== _% _%))) ! identical expressions predicate ) ( ! prove commutativity of addition ... ! first we prove equivalent axioms pa0,pa1, ! then we prove id successor valid clause ids, ! finally we prove the commutativity valid clause. ! prove alternative addition clauses pa0,pa1 valid wrt n0,n1,p0,p1,id: (pa0 ((_p _% _0 _%) (_n _%)) _induc 1 _ (pa0_n0 ((_p _0 _0 _0)) p0 1 n0) (pa0_n1 ((_p (_s _%) _0 (_s _%)) (_n _%)) p1 1 pa0) ) (pa1 ((_p _%1 (_s _%2) (_s _%3)) (_p _%1 _%2 _%3)) _induc 1 _ (pa1_p0 ((_p _0 (_s _%) (_s _%)) (_n _%)) p0 1 n1) (pa1_p1 ((_p (_s _%1) (_s _%2) (_s (_s _%3))) (_p _%1 _%2 _%3)) p1 1 pa1) ) (_axset PA (n0 n1 pa0 pa1 id) ! define alt. addition ax as equiv ! prove orig addition axioms p0,p1 valid wrt alt ax PA = n0,n1,pa0,pa1,id (p0 ((_p _0 _% _%) (_n _%)) _induc 1 PA (p0_n0 ((_p _0 _0 _0)) pa0 1 n0) (p0_n1 ((_p _0 (_s _%) (_s _%)) (_n _%)) pa1 1 p0) ) (p1 ((_p (_s _%1) _%2 (_s _%3)) (_p _%1 _%2 _%3)) _induc 1 PA (p1_pa0 ((_p (_s _%) _0 (_s _%)) (_n _%)) pa0 1 n1) (p1_pa1 ((_p (_s _%1) (_s _%2) (_s (_s _%3))) (_p _%1 _%2 _%3)) pa1 1 p1) ) ) ! prove this "id successor" valid clause (ids ((_== (_s _%a) (_s _%b)) (_== _%a _%b)) _induc 1 _ (ids_id ((_== (_s _%) (_s _%))) id) ) ! now prove the commutativity clause: (com ((_== _%3a _%3b) (_p _%1 _%2 _%3a) (_p _%2 _%1 _%3b)) _induc 1 _ (com1_p0 ((_== _% _%3b) (_n _%) (_p _% _0 _%3b)) _induc 2 PA (com12_pa0 ((_== _% _%) (_n _%) (_n _%)) id (_ _)) ) (com1_p1 ((_== (_s _%3a') _%3b) (_p _%1' _%2 _%3a') (_p _%2 (_s _%1') _%3b)) _induc 2 PA (com12_pa1 ((_== (_s _%3a') (_s _%3b')) (_p _%1' _%2 _%3a') (_p _%2 _%1' _%3b')) ids 1 com) ) ) ) %laxsl %lvcP). SOLUTIONS: Addition_is_Commutative time, #solns: 19.68 1 max stack size, max solve fn depth, # occur chks: 4919353 179252 28177368

back to Axiomatic Language Home Page