Detecting non-provable goals

DOI10.1007/3-540-58156-1_16MaRDI QIDQ5210774zbMATH OpenOpenAlexFDO

Authors Stefan Brüning

Publication date 21 January 2020

Published in Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-58156-1_16

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 475191
• A family of goal directed theorem provers based on conjunction and implication. I
• scientific article; zbMATH DE number 1508927
• A decision procedure for propositional N-Prolog
• scientific article; zbMATH DE number 3984612

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• An analysis of loop checking mechanisms for logic programs
• Controlling recursive inference
• Deriving descriptions of possible values of program variables by means of abstract interpretation
• Detecting non-provable goals
• scientific article; zbMATH DE number 4110158 (Why is no real title available?)
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 1348461 (Why is no real title available?)
• scientific article; zbMATH DE number 516986 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• Mechanical Theorem-Proving by Model Elimination
• Properties of substitutions and unifications
• Resolution methods for the decision problem
• Satisfiability of the smallest binary program
• SETHEO: A high-performance theorem prover
• Theorem proving with abstraction

Cited in

(3)

• Unprovability results for clause set cycles
• scientific article; zbMATH DE number 1341464 (Why is no real title available?)
• Detecting non-provable goals

Describes a project that uses

Uses Software

• SETHEO

This page was built for publication: Detecting non-provable goals

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