Theorem proving with abstraction

DOI10.1016/0004-3702(81)90015-1MaRDI QIDQ1149799zbMATH OpenOpenAlexDBLPWikidataFDO

Authors David A. 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

clausesresolution proofsset-of-support strategies

Mathematics Subject Classification ID

Cites work

• A paradigm for reasoning by analogy
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• scientific article; zbMATH DE number 3690750 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3278281 (Why is no real title available?)
• scientific article; zbMATH DE number 3343519 (Why is no real title available?)
• scientific article; zbMATH DE number 3359807 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Non-resolution theorem proving
• Planning in a hierarchy of abstraction spaces
• Unit Refutations and Horn Sets

Cited in

(25)

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

This page was built for publication: Theorem proving with abstraction

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