1. Introduction
This webpage describes a proof checker for axiomatic language
and is a supplement to this proof paper.
(A review of axiomatic language can be found
here.)
The proof checker is defined for and is written in a
restricted form of axiomatic language called
SAL - "Simplified Axiomatic Language".
A proof to be checked is expressed as an SAL query
and its successful solution confirms that the proof is correct.
The sections below give an overview of the system.
2. GAL / SAL / PAL - Forms of Axiomatic Language
In regular axiomatic language, called "General Axiomatic Language" - GAL,
string variables can occur anywhere within a sequence.
This enables concise definitions of common list predicates:
(member %x ($1 %x $2)). ! x is member of a sequence
(concat ($1) ($2) ($1 $2)). ! concatenation of two sequences
(append1 ($) %x ($ %x)). ! append one expr to end of sequence
(reverse () ()). ! reverse of a sequence
(reverse (% $seq) ($rev %))<
(reverse ($seq) ($rev)).
Example 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 ($')).
(reverse () ()).
(reverse (% $seq) %rev')<
(reverse ($seq) %rev),
(append1 %rev % %rev').
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.
PAL is used for data representation and processing inside the proof checker.
3. Encoding Axioms and Clauses
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 and expression and string variables be represented by
symbols starting with @ # *, respectively, and actual syntax-extension
symbols are represented as themselves, but can't begin with @ # *.
actual tokens encoded tokens
`x @x -- atoms
%a #a -- expression vars
$1 *1 -- string vars
abc abc -- syntax extension symbols
- can't start with @ # *
An 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 #))
4. The Check Predicate
A proof is defined in a "check" predicate which is then executed as
an SAL query.
The proof representation language is thus an embedded DSL with SAL as host.
A successful query solution indicates that the proof is correct.
The check predicate and its four arguments are as follows:
check - check proofs of valid clauses derived from a set of axioms
(check <axs> - labeled axioms with labeled subsets (encoded SAL)
<chk_steps> - check clause proofs and equiv ax subset proofs
<axsl> - final ax set clause and subset labels
<lvcP> - final labeled (axiom & proved) valid clauses (PAL)
)
See the proof paper for the
proof inference rules.
This comment block from the
SAL check.ax source file shows the representation of "inference proofs"
(rules R1-R4,R8) and induction proofs (R9) and the representation
of axiom subset equivalence proofs.
5. Example Proofs
This section gives example proofs that are actual executions of the
check predicate using the SAL query solver.
We use single letter predicate names below in place of longer
symbol names for conciseness.
5.1. Q Numbers
"Q numbers" are just natural numbers with a "q" predicate name.
They can be defined independently from "N numbers" using the
q0,qs axioms below, or they can be defined directly from N numbers
using the qn axiom. The following SAL query shows that axiom
subsets for these two definitions are equivalent:
! qnum4.q - check "q num" equiv axiom set proof
! - "q nums" are natural numbers with "q" predicate name
(%laxsl %vclbls)< ! query output is axiom set and valid clause labels
(check ! check proof of equivalent q num definition
( ! axiom set
(n0 ((n 0))) ! 0 is natural number
(ns ((n (s #)) (n #))) ! successor of n is nat num, if n is nat num
(Q ! named ax subset for "q num" definition
(q0 ((q 0))) ! 0 is q num
(qs ((q (s #)) (q #))) ! successor of q num is q num
)
)
( ! check steps:
! prove that q num can be defined from "n num"
(qn ((q #) (n #)) `ind 1 _ ! induction against orig ax set (w Q subset)
(qn_n0 ((q 0)) q0)
(qn_ns ((q (s #)) (n #)) qs 1 qn)
)
! prove that Qn={qn} is an equivalent alternative ax subset for Q={q0,qs}
(`axss Q (Qn qn)
! prove original ax subset Q={q0,qs} wrt new ax subset Qn
(q0 ((q 0)) qn 1 n0)
(qs ((q (s #)) (q #)) `ind 1 _ ! induction against axioms w Qn subset
(qs_qn ((q (s #)) (n #)) qn 1 ns)
)
)
) %laxsl %lvcP),
(transpose %lvcP (%vclbls %vcP)).
The axiom set above gives the natural number axioms n0,ns and a "Q"
axiom subset q0,qs that defines the q nums. The check steps first
prove that the qn clause defining q nums from n nums is valid
with respect to the q0,qs axioms. The `axss block then shows
that the q0,qs clauses are valid with respect to the Qn = {qn}
axiom subset, thus showing that the two subsets Q and Qn are
equivalent. The single solution for this query is as follows:
SOLUTIONS:
((n0 ns (`alt (Q q0 qs) (Qn qn))) (n0 ns q0 qs qn))
time, #solns: 5.72 1
max stack size, max solve fn depth, # occur chks: 1454397 52930 4736731
The solution expression shows the labels of axioms and axiom subsets.
Note that the Qn = {qn} subset in the `alt expression has been added
as an equivalent alternate subset for the Q subset. The solution
expression then shows the labels of the valid clauses, which are
the original axioms plus the proved qn clause. Note that we used
the 'transpose' utility to extract the labels of the valid clauses
without getting a complete dump of their PAL definition.
The computation time was 5.72 seconds. Changing all the syntax-extension
symbols to atoms would have made this several times faster.
The max stack size and other output parameters can be ignored.
5.2. Commutativity of Natural Number Addition
To express commutativity of addition we need the following utility
predicate that asserts that two expressions are identical:
(== % %). ! argument expressions are identical
The commutativity of addition is proved by proving the following clause:
(= %3a %3b)< (p %1 %2 %3a), (p %2 %1 %3b).
This clause asserts that the two additions, which have their
arguments in opposite order, always give identical results.
(Otherwise, a generated expression is not a valid expression
so this clause would not be valid.)
To prove this clause valid we need to use alternative
addition definitions -- one with recursion on the first argument
and the other with recursion on the second.
The following SAL query gives the proof:
(%laxsl %vclbls)< ! query output is axiom set and valid clause labels
(check ! check proof for addition commutativity
( ! axiom set
(= ((= # #))) ! identical expressions
(n0 ((n 0))) ! 0 is natural number
(ns ((n (s #)) (n #))) ! successor of n is nat num, if n is nat num
(P ! named ax subset for plus (recursion on 1st arg)
(p0 ((p 0 # #) (n #))) ! 0 + n = n
(ps ((p (s #1) #2 (s #3)) (p #1 #2 #3))) ! n1+1 + n2 = n3+1
! if n1 + n2 = n3
)
)
( ! check steps:
! pairs with same 1st elems are identical if 2nd elems are identical
(=2 ((= (# #a) (# #b)) (= #a #b)) `ind 1 _ ! do induction on 1st cond
(=2_= ((= (# #2) (# #2))) =)
)
! prove alternative plus axioms (recursion on 2nd arg)
(pa0 ((p # 0 #) (n #)) `ind 1 _ ! n + 0 = n
(pa0_n0 ((p 0 0 0)) p0 1 n0)
(pa0_ns ((p (s #) 0 (s #)) (n #)) ps 1 pa0) ! unfold w induc hypoth!
)
(pas ((p #1 (s #2) (s #3)) (p #1 #2 #3)) `ind 1 _ !n1+n2+1=n3+1 if n1+n2=n3
(pas_p0 ((p 0 (s #) (s #)) (n #)) p0 1 ns)
(pas_ps ((p (s #1) (s #2) (s (s #3))) (p #1 #2 #3)) ps 1 pas)
)
! define equivalent alternative plus axiom subset Pa = pa0,pas
(`axss P (Pa pa0 pas)
! prove original ax subset P wrt new ax subset Pa
(p0 ((p 0 # #) (n #)) `ind 1 _ ! (Pa replaces P in ax set)
(p0_n0 ((p 0 0 0)) pa0 1 n0)
(p0_ns ((p 0 (s #) (s #)) (n #)) pas 1 p0)
)
(ps ((p (s #1) #2 (s #3)) (p #1 #2 #3)) `ind 1 _
(ps_pa0 ((p (s #) 0 (s #)) (n #)) pa0 1 ns)
(ps_pas ((p (s #1) (s #2) (s (s #3))) (p #1 #2 #3)) pas 1 ps)
)
) ! thus, P and Pa ax subsets are equivalent!
! prove commutativity of addition!
(c ((= #3a #3b) (p #1 #2 #3a) (p #2 #1 #3b)) `ind 1 _P ! induc on P subset
(c_p0 ((= # #3b) (n #) (p # 0 #3b)) `ind 2 _Pa ! induc on Pa subset
(c_p0_pa0 ((= # #) (n #) (n #)) = (_ _)) ! adding conditions to =
)
(c_ps ((= (s #3a') #3b) (p #1 #2 #3a')
(p #2 (s #1) #3b)) `ind 2 _Pa
(c_ps_pas ((= (s #3a') (s #3b')) (p #1 #2 #3a')
(p #2 #1 #3b')) =2 1 c)
)
)
) %laxsl %lvcP),
(transpose %lvcP (%vclbls %vcP)).
The query solution output shows that commutativity has been proved:
SOLUTIONS:
((= n0 ns (`alt (P p0 ps) (Pa pa0 pas))) (= n0 ns p0 ps =2 pa0 pas c))
time, #solns: 32.40 1
max stack size, max solve fn depth, # occur chks: 8519162 308361 50166183
The solution output shows that addition axiom subset P is equivalent to
subset Pa and that the commutativity clause c has been proved valid.
back
to Axiomatic Language Home Page