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

DOI10.1007/BF01880327MaRDI QIDQ1181711zbMATH OpenFDO

Authors Dov Gabbay, Frank Kriwaczek

Publication date 27 June 1992

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

Full work available at URL https://doi.org/10.1007/BF01880327

zbMATH Keywords

classical logicgoal-directed theorem proverintermediate logicintuitionistic logicPrologresolutionrestart rule

Mathematics Subject Classification ID

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

Recommendations

• A decision procedure for propositional N-Prolog
• An Intuitionistic Predicate Logic Theorem Prover
• Theorem proving for conditional logics: CondLean and GOALDUCK
• scientific article; zbMATH DE number 1543301

Cites work

• Computation with run time skolemisation (N-Prolog part 3)
• scientific article; zbMATH DE number 512976 (Why is no real title available?)
• N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure
• Near-Horn prolog and beyond
• Semantical investigations in Heyting's intuitionistic logic

Cited in

(9)

• Theorem proving for intensional logic
• Analyzing rule sets for the calculation of banking fees by a theorem prover with constraints
• Theorem proving for conditional logics: CondLean and GOALDUCK
• scientific article; zbMATH DE number 4104409 (Why is no real title available?)
• Computation with run time skolemisation (N-Prolog part 3)
• Towards structurally-free theorem proving
• scientific article; zbMATH DE number 1543301 (Why is no real title available?)
• A decision procedure for propositional N-Prolog
• Detecting non-provable goals

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1181711)