希望能够实现自我推理。
The main predicate of your program is
to be prove/1 which is to take a list of sequents as argument and determine whether every sequent in the list can be proved.
举例： prove([[neg(p or q)] seq [neg p]]) 输出 ”Yes”.
大致思路应该是下图没错但是因为时间紧张之前又没有接触过prolog，特来求教
% THIS PROGRAM SUPPOSES A CORRECT INPUT OF THE FORM
% 'sequent = list1 seq list2', WHERE 'list1', 'list2' DO
% NOT CONTAIN 'seq' AS A SUBSTRING
% define logical operations
:-op(800, xfx, seq). % syntactic entailment
:-op(700, xfy, iff). % biconditional
:-op(600, xfy, imp). % implication
:-op(400, yfx, and). % conjunction
:-op(400, yfx, or). % disjunction
:-op(300, fy, neg). % negation
% equivalence(+Formula1, +Formula2)
% equivalence between formulae
equivalence(neg (P and Q), (neg P) or (neg Q)).
equivalence(neg (P or Q), (neg P) and (neg Q)).
equivalence(P imp Q, (neg P) or Q).
equivalence(P iff Q, (neg P and neg Q) or (P and Q)).
% con_concat(+List, -Conjunction)
% transforms a list of formulae into a conjunction
???
% dis_concat(+List, -Disjunction)
% transforms a list of formulae into a disjunction
???
% preprocess(+Seq, -Prep_Seq)
% preprocesses the left and right lists of formulas in a sequent
% e.g. '[neg (p1 or p2), p3] seq [p4 and p5, p6, p7]' is the same as
% '(neg (p1 or p2)) and (p3) seq (p4 and p5) or (p6) or (p7))'
???
% rewrite_sequent(+Seq, -NewSeq, -Tree)
% rewrites a sequent applying the rules P2a-P6b
% and returns the result together with its proof tree
???
% theorem(+Seq)
% check whether a sequent is a theore by applying rule P1
???
% prove_sequent(+Seq, -Tree)
% proves a sequent, prints its tree
???
% print_sequent(+Tree)
% printing the proof in a tree-like shape
???
% prove(+L).
% proves a list of seqeunts
???
