LEANT(A)P - LEAN TABLEAU-BASED DEDUCTION

被引：68

作者：

BECKERT, B ^{[1
]}

POSEGGA, J ^{[1
]}

机构：

[1] UNIV KARLSRUHE,INST LOG KOMPLEXITAT & DEDUKT SYST,D-76128 KARLSRUHE,GERMANY

来源：

JOURNAL OF AUTOMATED REASONING | 1995年 / 15卷 / 03期

关键词：

LOGIC FOR ARTIFICIAL INTELLIGENCE; THEOREM PROVING; AUTOMATED DEDUCTION; SEMANTIC TABLEAUX; FIRST-ORDER LOGIC; PROLOG;

D O I：

10.1007/BF00881804

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

''prove((E,F),A,B,C,D) :- !, prove(E, [F\A],B,CD). prove((E;F),A,B,C,D) :- !, prove(E,A,B,C,D), prove(F,A,B,C,D). prove(all(H,I),A,B,C,D) :- ! \+ length(C,D), copy-term((H,I,C), (G,F,C)), append(A,[all(H,I)],E), prove(F,E,B,[G\C],D). prove(A,-, [C\D],-,-) :- ((A = -(B); -(A)=B)) --> (unify(B,C); prove(A,[],D,-,-)). prove(A,[E\F],B,C,D) :- prove(E,F,[A\B],C,D).'' implements a first-order theorem prover based on free-variable semantic tableaux. It is complete, sound, and efficient.

引用

页码：339 / 358

页数：20