A family of goal directed theorem provers based on conjunction and implication. I

DOI10.1007/BF01880327zbMath0743.03009MaRDI QIDQ1181711

Dov M. Gabbay, Frank Kriwaczek

Publication date: 27 June 1992

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

resolutionintuitionistic logicPrologclassical logicintermediate logicgoal-directed theorem proverrestart rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17) Subsystems of classical logic (including intuitionistic logic) (03B20) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04) Intermediate logics (03B55)

Related Items (1)

Computation with run time skolemisation (N-Prolog part 3)

Cites Work

• Unnamed Item
• Near-Horn prolog and beyond
• Semantical investigations in Heyting's intuitionistic logic
• N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure
• Computation with run time skolemisation (N-Prolog part 3)

This page was built for publication: A family of goal directed theorem provers based on conjunction and implication. I