78

数理解析研究所講究録
第1186巻 2001年 78-83

PROOF CHECKING USING PROLOG

MAKOTO TSUKADAABSTRACT.
A proof system for propositional and predicate logic isdiscussed. As a meta‐language specifying the system, a logic program‐ming language, namely, Prolog is adopted. All of proof rules, axioms,definitions, theorems and also proofs can be described as predicates ofProlog.

1.

INTRODUCTION

Proof is a way of showing that something is true. It is a process of reasoning
to reach a desired fact by using general rules and some facts already shown. In
natural deduction we have a collection of proof rules. The most useful proof rules
may be so‐called modus ponens which infers the formula Q from two premises oneof which is a formulas P and the other is a formula Parrow Q . In this paper we
introdue a notion of the tablet on which we construct a calulus for reasoning about
propositions by natural deduction. The tablet is a stack‐like memory on which
formulas are piled. The operations push and pop act at the top of the memory sameas the usual stack, however not only the top of the items but also each item in thetablet can be refered at any time. All proof rules, axioms, definitions, theorems andtheir proofs are discribed as operations accessing the tablet. For example, modus
ponens is considered as an operation which places the formula Q on the tablet if theformula P and also Parrow Q already exist on it.
We adopt a logic programming language, namely, Prolog, as a meta‐language
system to describe mathematics. A program of Prolog is a series of the Hormclauses. A Horn clause is in general of the form
P:- Q_{1}, Q_{2},\ldots,Qn.

This is called a rule and means that P succeeds when all of Q_{1}, Q_{2},\ldots

and Q_{n}n=0 we denote it by `\zeta P. ” instead of “ P :‐.”, and call it asucceed. In the case offact. The following is an example of mathematical description using Prolog.
constant (socrates).
variable (x).

formula (Xis_{-}a_{-}man )formula (Xis_{-}a_{-}morta1 ):—term (X).

:—term (X).

2000 Mathematics Subject Classification. 03B35,68T15 .
Key words and phrases. proof theory, theorem proving, proof checker, Prolog.
「計算機による解析学における論理計算」 として講演した内容の—部である

79

axioml :‐then forall ( x,xis_{-a_{-^{m}}}an imp xiS_{-a_{-^{mort1)}}}a .
axiom2:‐ then socrates

theoreml

is_{-}a-man .

:‐ then socrates

is_{-}a-morta1 .

proofl :‐forall( x,xis_{-a_{-^{m}}}an imp

xis_{-}a_{-}morta1 )by axioml,

socrates is_{-^{a_{-man}}} imp socrates is_{-}a_{-^{m}}orta1

by sp ( xis_{-a_{-^{m}}}an imp xis_{-}a_{-^{m}}orta1,X , socrates) ,socrates is_{-}a_{-m}an by axiom2,
i_{S_{-}a_{-}}morta1

socratesby mp (socrates

is_{-^{a_{-man}}} , socrates

i_{S_{-}a_{-^{mo}}}rta1 ).

We need a lot of built‐in predicates, which make proofl be a valid proof of theoreml.
2.

SYNTAX ANALYSIS OF FORMULAS

We have first to develope a language in which each sentence is argued to betrue or false. Such a sentense is called a formula. The BNF (Backus‐Nauer Form) isoften used when the language is of context free. In predicate logic the collection ofclosed formulas (formulas in which all variables are dominated) is context sensitive,

because every variable in a formula has its own scope. In this case we can not use
the BNF.

Let FORMULA be the set of P' s such that formula (P) succeeds under‐ thefollowing \dot{f}acts and rules.

constant (socrates).

term (X): ‐ const ant (X).

formula (X is_{-}a_{-}man )f ormula (X:‐term (X).

iS_{-^{a}-^{mort}}a1 )formula (not P):-t erm (X).
:‐formula (P).

formula ( P and Q) :‐formula (P) , formula (Q).
formula ( p or Q) :‐formula(P) , formula(Q).
formula ( p imp Q) :‐formula (P) , formula (Q).
ThenFORMULA={socrates

is_{-^{a}-^{m}}an ,socrates

i_{S_{-}a_{-}mo}rta1 ,not socrates is_{-}a_{-^{man}} , not socrates i_{S_{-}a}-morta1 ,socrates

i_{S_{-}a_{-}}man

and socrates

is_{-}a_{-^{man}} ,. . .}In order to treat equalities, the first order predicate logic and set theory, we must

further add some other following clouses.
variable (x).

variable (y).
variable (z).
constant([]) .

formula (X=Y) :‐term (X) , term (Y).
formula (X in Y) :‐term (X) , term(Y).

80

formula( x subseteq Y) :‐term(X) , term (Y) .
(forall(x,P)):variable (X) , substitute ( P,X=[] , Q) , formula(Q).
formula (forSome(x,p)):variable (X) , substitute ( P,X=[] , Q) , formula(Q).
term (setof(X,p)):variable (X) , substitute ( P,X=[] , Q) , formula(Q).
formula[] is a dummy constant. substitute ( P,X=[] , Q) succeeds whenever Q is unified
with the formula obtained by replacing each occurrences of term X or free occurrencesof variable X in P with [] . For instance, we like to denote \forall x(x=x A \exists y(x=y\vee x\in\{x|X=y\})) byforall( x,X^{=}X and forsome( y,x=y orx

in setof (x,x=y) )),which is a formula because[]=[] and forsome ( y, []=y or [] in setof (x,x=y) )is a formula without free variable occurrence, namely, a closed formula.
3.

THE PREDICATE ` if/1 ’ AND ` then/1 ’

In our system the prefixed predicates if/1 and then/1 play central roles. if isdefined as follows.

ifP:‐formula(P) , tablet (P).

ifP:‐tablet (suppose (p) ).

then P succeeds whenever either formula P or suppoese (P) is in the tablet.
thenP:‐formula (P) , asserta (tablet(P)) .

then P succeeds whenever P is a formula and has a side effect by which P is pushed
onto the tablet. Using the predicate if/1 and then/1 above we can express a proof
rule such that\frac{P_{1}P_{2}\cdots P_{n} {Q}as follows.

if P_{1} , if P_{2},\cdots

Especially the proof rule of modus ponens
mp(P,Q) :‐ if

P,ifP, if P_{n} , then Q .

\frac{PParrow Q}{Q}MP is denoted by

imp Q , then Q.

A proof rule without if‐part is called a axiom or a scheme of axioms.
In order to treat the logic with equalities we need a scheme of axioms such thateql (X) :‐term(X) , then X eq X.

and also a proof rule such that81

eq2 (P,x=Y, Q):‐ifP,

if

X=Y ,substitute (P,x=Y, Q) , then Q.

The followings are proof rules necessary for predicate logic.
sp (P,X=Y) : ‐if forall (X. P) , term(Y) , substitute (P,X=Y, Q) ,then Q.

P(Y),gen (P,X=Y) :‐if, term (X) , variable. substitute (P,X=Y,Q) ,then forsome
.

(Y,Q)

For example, ifforall ( x,xis_{-}a_{-^{man}} imp

xi_{S_{-^{am}}}-orta1 )can be found in the tablet,sp ( xis_{-a_{-^{m}}}an

imp xis_{-}a_{-mo}rta1,X^{=_{Soc}}rateS )succeeds and pushes
socrates is_{-}a_{-^{man}} imp socrates i_{S_{-}a_{-}}morta1

onto the tablet. On the other hand, if it is in the tablet,sp ( soCratesis_{-}a_{-^{man}}

imp socrates i_{S_{-^{a_{-}m}}}orta1, SocrateS^{=}x )succeeds and pushes
forsome ( x,xis_{-}a_{-^{man}} imp

xi_{S_{-^{am}}}-orta1 )onto the tablet.

s_{EMANT}ICs OF PROPOSITIONAL LOGIC

4.

Semantics of propositional logic is of truth values. We consider a formula P to
be true, whenever the predicate if P succeeds.
is‐true(P):— if P.

Conversely if P is true, then P can be piled on the tablet. Therefore we have thefollowing proof rule.
truth‐value (P): ‐ is‐true (P) , then P.

Moreover the system have the following built‐in facts and rules. These are of thetruth tables.
formula (true).

formula (false).

is‐true (true).

is‐false (false).

is‐true (P) :‐is‐false (P).
is‐false(P) :‐ is‐true(P)is‐true ( p imp Q) :‐is‐true (P) , is‐true (Q).
is‐false ( P imp Q) :‐is‐true (P) , is‐false (Q).
is‐true ( P imp Q) :‐is‐false (P) , is‐true (Q).
is‐true ( P imp Q) :‐is‐false (P) , is‐false (Q).

82

We also have the truth tables for the logical conjunctions and,or and eqv .

We can place some phrases on the tablet, which themselves are not formulas.
begin‐suppose (P) :‐formula(P) , asserta(tablet (suppose (p) )).

The predicate begin‐suppose (P) succeeds and the phrase suppose (P) is pushed
on the tablet whenever P is a formula. The prefixed predicate begin_{-}suppoSe/1

opens a suppose block on the tablet and this block must be closed by the predicate
end_{-\sup po}se/0 . In this block, we can treat P as a true formula. Out of the block,
we refer the formula Q in the block as a true formula P imp Q.

begin‐forall (X) :‐variable (X) , asserta ( atblet (forall (X))).

The predicate begin‐forall (X) succeeds and the phrase forall (X) is pushed
on the tablet whenever X is a variable. The prefixed predicale begin_{-}foral1/1

opens a forall block on the tablet and this block must be closed by the predicate

end_{-}foral1/0 . In this block, we can treat X as a constant. Out of the block, werefer the formula Q in the block as a true formula forall (X, Q).

We also have the other kind of block called a forsome block. If the top of
the tablet is a formula forsome (X, P), then such a block canbe opened using theprefixed predicate begin-forsome/1 and imediately pushed P on the tablet. This
block must be closed by the predicate end_{-}f_{0}rSome/0 . In this block, we can treat
X as a constant and P is a true formula. Out of the block, we refer the formula Q in

the tablet as a true formula in itself only if X does not occur in Q as a free variable.
3.

p_{ROOF}S OF THEOREMS

Let us prove theoreml under axioml and axiom2 as follows.
axioml :‐then forall ( x,xaxiom2:‐ then socrates

theoreml

is_{-}a −manimp

xis_{-}a_{-^{m}}orta1 ).

is_{-}a-man .

:‐ then socrates

is_{-^{a}-^{mor}}ta1 .

Because we consider proving theoreml as coding a program which places the formulasocrates

is_{-}a_{-}morta1 on the tablet, the following is a proof of theoreml.

proofl :‐axioml,sp ( X

is_{-}a −manimp

xis_{-}a_{-^{m}}orta1,X , socrates) ,axiom2,mp (socrates

is_{-}a-man , socrates

is_{-}a_{-^{m}}orta1 ).

After proofl succeeds, the tablet becomes as follows.
tablet (socrates is_{-}a_{-^{m}}orta1 ).

tablet (socrates is_{-}a_{-}man ).

tablet (socrates is_{-}a_{-^{man}} imp socrates is_{-^{a}-or}mta1 ).
tablet (forall ( x,x is_{-}a−man imp xiS_{-}a_{-^{mor}}ta1 )).

In order to make a proof look like usual proofs which we write down on a notebookor a black board, we prepare an infixed predicate by/2 . P by A succeeds wheneverA succeeds and also the top of the tablet is P. Indeed, P by A is definec as follows.

83

P by A:-A , top (P).
top (P) :‐tablet (P) , ! , X=Y .

Using the predicate by/2 , we can write a proof of theoreml as follows.
proofl :‐forall( x,Xsocrates

by sp ( xis_{-}a −manimp

xis_{-}a_{-}morta1 )is_{-}a −man imp socrates
is_{-}a −man

imp xiS_{-}a_{-^{mor}}ta1,x , socrates) ,socrates

is_{-}a −man by axiom2,socrates

is_{-^{a}-^{mor}}ta1

by mp (socratesby axioml,

is_{-^{a}-^{mor}}ta1

is_{-}a-man , socrates

is_{-}a_{-}morta1 ).

REFERENCES

1. M. Huth and M. Ryan, Logic Computer Science: Modelling and reasoning about systems, Cam‐bridge, 2000.

2. Y. Nakamura, A Language System for Description of Mathematics ‐THEAX‐ (in Japanese),
Department of Information Engineering, Shinshu University, 1985.

DEPARTMENT OF INFORMATION SCIENCES, TOHO UNIVERSITY, FUNABASHI, CHIBA 274‐
8510, JAPAN..
E‐mail address:

tsu.kada@is.Sci.t_{oh-}ou.ac.j_{P}