A decision procedure for propositional N-Prolog

DOI10.1007/BFB0038697MaRDI QIDQ5053010zbMATH OpenFDO

Authors Jörg Hudelmaier

Publication date 26 November 2022

Published in Extensions of Logic Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Logic programming (68N17) Subsystems of classical logic (including intuitionistic logic) (03B20) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A family of goal directed theorem provers based on conjunction and implication. I
• \(N\)-Prolog and equivalence of logic programs. I
• A decision procedure revisited: Notes on direct logic, linear logic and its implementation
• Some applications of Gentzen's proof theory in automated deduction
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic

Cited in

(9)

• N-Prolog: An extension of Prolog with hypothetical implications. I.
• N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure
• scientific article; zbMATH DE number 63752 (Why is no real title available?)
• Computation with run time skolemisation (N-Prolog part 3)
• scientific article; zbMATH DE number 4130365 (Why is no real title available?)
• Detecting non-provable goals
• Some applications of Gentzen's proof theory in automated deduction
• scientific article; zbMATH DE number 4145871 (Why is no real title available?)
• A decision procedure revisited: Notes on direct logic, linear logic and its implementation

This page was built for publication: A decision procedure for propositional N-Prolog

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