Theorem proving with abstraction

DOI10.1016/0004-3702(81)90015-1zbMath0454.68113DBLPjournals/ai/Plaisted81OpenAlexW2025339139WikidataQ30052608 ScholiaQ30052608MaRDI QIDQ1149799

David Alan Plaisted

Publication date: 1981

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(81)90015-1

zbMATH Keywords

resolution proofsclausesset-of-support strategies

Mathematics Subject Classification ID

Related Items (23)

Automatically generating abstractions for planning ⋮ Downward refinement and the efficiency of hierarchical problem solving ⋮ Man-machine theorem proving in graph theory ⋮ Octopus: combining learning and parallel search ⋮ Speeding up inferences using relevance reasoning: a formalism and algorithms ⋮ Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs ⋮ Analogical logic program synthesis algorithm that can refute inappropriate similarities ⋮ First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation ⋮ A simplified problem reduction format ⋮ Towards a practical theory of reformulation for reasoning about physical systems ⋮ Proving theorems by reuse ⋮ Reasoning about model accuracy ⋮ A theory of abstraction ⋮ Detecting non-provable goals ⋮ Abstraction for non-ground answer set programs ⋮ On an unsatisfiability-satisfiability prover ⋮ Building proofs or counterexamples by analogy in a resolution framework ⋮ Interpreting Abstract Interpretations in Membership Equational Logic ⋮ Conceptual fuzzy sets and their connectives ⋮ The inevitability of inconsistent abstract spaces ⋮ A relevance restriction strategy for automated deduction ⋮ Frameworks for abstract interpretation ⋮ Data abstractions for decision tree induction

Cites Work

• Non-resolution theorem proving
• Planning in a hierarchy of abstraction spaces
• A paradigm for reasoning by analogy
• Unit Refutations and Horn Sets
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Theorem proving with abstraction