Help for the logic programming software 

This software permits you to check a proof by contradiction you did by 
hand. The notation that is used is based on logic programming. In the 
proof, you are allowed to use 4 inference rules: the negation of the 
goal rule, the resolution rule, the factorization rule and the 
contradiction rule. 

The rules are expressed using the following notation: 

P1 ... Pn 
--------- 
C 

where P1,..., Pn are the premises and C is the conclusion deduced 
from P1,...,Pn. 

* The negation of the goal rule is the following: 

g 
-- 
<-g 

The negation of the goal rule takes one premise. 

* The resolution rule is the following: 

p1 <- q1,...,qn         <- p1,p2,...,pm 
--------------------------------------- 
<- q1,...,qn,p2,...,pm 

The resolution rule takes two premises. 

* The factorization rule is the following: 

q <- p1,p1,p2,...,pn 
------------------ 
q <- p1,p2,...,pn 

The factorization rule takes one premise. 

* The contradiction rule is the following: 

<- p p <- 
-------------------- 
0 (zero denotes the contradiction) 

The contradiction rule takes two premise. 

Here is the way to check a proof: 

Begin by entering all the clauses. Enter a clause and click on Save 
C.... 

Then you can input the goal to prove. The goal does not contain any 
arrow. Enter a goal and then click on Save G... 

Now you can begin to check the proof of the goal with respect to the 
clauses you entered. A number is associated with the clauses and the goal. 

Check an inference by entering the number of the clause(s) (premises) 
involved in the inference, selecting the inference rule, entering the 
conclusion and clicking Verify. 

Some examples to test:

mortalSocrates <- manSocrates
manSocrates <-
Prove that mortalSocrates is true.

square <- rectangle, equalsides
rectangle <- parallelogram, rightangles
parallelogram <-
rightangles <-
equalsides <-
Prove that square is true.

takeumbrella <- itrains
itrains <-
Prove that takeumbrella is true.

catFelix <- FelineFelix, mammalFelix 
hasclawsFelix <-
FelineFelix <- whiskeredFelix, hasclawsFelix
mammalFelix <-
whiskeredFelix <-
Prove that catFelix is true.

p<-q,r
t<-p,s
s<-a,b
a<-
b<-
q<-
r<-
Prove that t is true.

k<-r,a
r<-u,w
u<-
w<-a
a<-b,c
b<-
c<-
Prove that k is true.

Have fun!