% File : QUIP % Author : Dave Plummer % Written: 23 January 1985 % Updated: 24 January 1985 % Purpose: simple resolution theorem prover for AI1 project % The code in this file implements QUIP (QUIck Prover), a resolution % theorem prover, in PROLOG. For those unfamiliar with theorem % proving a quick explanation is given below, for more detail see % "The Computational Modelling of Mathematical Reasoning" by Alan Bundy. % % QUIP proves theorems in a subset of propositional calculus. In this % calculus, propositions are represented by proposition letters, eg % a, b, f etc; Each letter may be thought of as abbreviating an % assertion about the world which is either true or false eg: % % "AI is the most interesting subject taught at Edinburgh University", % "Theorem proving is the most interesting area of AI", % "PASCAL is the best programming language in existence" % % The full propositional calculus also has connectives: "&", "v" "->", % "-". These correspond (roughly) to English words such as "and", % "or", "implies", and "not" respectively. Sentences are made from % proposition letters and connectives according to the following rules: % % i) any proposition letter is a sentence: % a b are both sentences % % ii) if "a" and "b" are sentences then: % a & b is a sentence; % a v b is a sentence; % a -> b is a sentence; % - a is a sentence; % % Thus if a abbreviates the sentence % "AI is the most interesting subject taught at Edinburgh University" % and b abbreviates the sentence % "Theorem proving is the most interesting area of AI", % then "a & b" abbreviates % "AI is the most interesting subject taught at Edinburgh University % and Theorem proving is the most interesting area of AI". % % Now we have defined the language that we will use, we should decide % how the truth of certain sentences affect others that are made out of % them. We would like this to reflect the everyday meanings we assign to % sentences; we will see that this is not easy, but a close approximation % is easily found. % % Consider the sentence "a & b" : we would like this sentence to be % true if both the sentences "a" and "b" are true. % Similarly, we would like "-a" to be true only when "a" is false. % % Consider the sentence "a v b" : we would definitely like this to % be true when one of "a" and "b" is true, and false when neither % is true. But what about when both are true? We choose that "a v b" % is true whenever "a" is true and "b" is true. (Maybe you could think % of some sentences in English which confirm this choice, and also % some that would refute it.) % % Implication causes a similar problem. We define the sentence "a -> b" % to be true if either "a" is false, or "b" is true. This definition % is quite counterintuitive. In everyday English, to say that: % "The sky is blue implies 2+2=4" % is nonsense, but in propositional calculus it is true. % % To summarize this, we can write out a 'truth table': % a b -a -b a & b a v b a -> b % true true false false true true true % true false false true false true false % false true true false false true true % false false true true false false true? % % Now we have to consider how to perform proofs in this system. From % here on we will assume that our language will contain only the % connectives "v" and "-". It turns out that any sentence which uses % the other connectives can be expressed in terms of a set of such % sentences, so we haven't lost anything by so doing. % % How do we deduce new sentences from old ones? Well we use a rule of % inference which is called resolution. The rule is quite simple and % is stated as follows: If you have two sentences and one is of the % form "a v b", and the other is of the form "-a v c", then you can % deduce the new sentence, "b v c". Let us first convince ourselves % that this is a reasonable rule. Both of the original sentences % contain "a" but in the second "a" is negated. % We know that "a v b" is true: if we assume that "a" is false, % then "b" must be true. So if "a" is false then "b" is true. % Now lets assume that "a" is true, then "-a" is false, and by % the second sentence (-a v c is true) "c" must be true. So if % "a" is true then "c" is true. But a must be either true or false % so either "b" or "c" must be true, that is "b v c" must be true. % % Hopefully I have now convinced you that the resolution rule deduces % only true sentences from true sentences. go :- read_hyps(Hyps), read_conc(Conclusion), prove(Hyps,Conclusion). read_hyps(Hyps) :- read(Clause), read_hyps(Clause,Hyps). read_hyps([],[]). read_hyps([H|T],[[H|T]|Rest]) :- read_hyps(Rest). read_conc([NegatedAtom]) :- read(Atom), complementary(Atom,NegatedAtom). prove(Clauses,InputClause) :- member(Clause,Clauses), resolve(Clause,InputClause,NewClause), prove1(NewClause,Clauses,InputClause). prove1([],_,_) :- nl,write('Proof Complete'). prove1(NewClause,Clauses,InputClause) :- prove([InputClause|Clauses],NewClause). resolve(Clause1,Clause2,Resolvent) :- select(Literal1,Clause1,RestClause1), select(Literal2,Clause2,RestClause2), complementary(Literal1,Literal2), union(RestClause1,RestClause2,Resolvent). complementary(-A,A). complementary(A,-A). select(X,[X|T],T). select(I,[H|T],[H|Rest]) :- select(I,T,Rest). union([],List,List). union([H|T],List,Union) :- member(H,List), union(T,List,Union). union([H|T],List,[H|UnionRest]) :- union(T,List,UnionRest). member(X,[X|_]). member(X,[_|T]) :- member(X,T). /* end of file */