A method for simultaneous search for refutations and models by equational constraint solving

DOI10.1016/S0747-7171(10)80014-8zbMath0770.68104MaRDI QIDQ1198235

Ricardo Caferra, Nicolas Zabel

Publication date: 16 January 1993

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

theorem provingresolutionequational theorydecision procedure

Mathematics Subject Classification ID

Related Items (max. 100)

The first order theory of primal grammars is decidable ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ A calculus combining resolution and enumeration for building finite models ⋮ A fast saturation strategy for set-theoretic tableaux ⋮ Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview ⋮ A meta-logic of inference rules: Syntax ⋮ Superposition for Fixed Domains ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ Analogy in Automated Deduction: A Survey ⋮ A method for building models automatically. Experiments with an extension of OTTER ⋮ Semantically guided first-order theorem proving using hyper-linking ⋮ Deciding the Inductive Validity of ∀ ∃ * Queries ⋮ Partial matching for analogy discovery in proofs and counter-examples ⋮ Building proofs or counterexamples by analogy in a resolution framework ⋮ Constructing infinite models represented by tree automata ⋮ Automated Model Building: From Finite to Infinite Models

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Seventy-five problems for testing automatic theorem provers
• Equational problems and disunification
• Using sophisticated models in resolution theorem proving
• A canonical form for generalized linear constraints
• On a bound for the complexity of terms in the resolution method
• Automated deduction by theory resolution
• Solvable cases of the decision problem
• Automated Theorem Proving: After 25 Years
• Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
• Resolution Strategies as Decision Procedures
• Automatic Theorem Proving With Renamable and Semantic Resolution

This page was built for publication: A method for simultaneous search for refutations and models by equational constraint solving