Model building with ordered resolution: Extracting models from saturated clause sets

DOI10.1016/S0747-7171(03)00028-2zbMath1019.03008MaRDI QIDQ1404975

Nicolas Peltier

Publication date: 25 August 2003

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

zbMATH Keywords

model buildingHerbrand modeltree automatonordered resolutionsatisfiable clause sets

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Representing and building models for decidable subclasses of equational clausal logic ⋮ Superposition for Fixed Domains ⋮ Deciding the Inductive Validity of ∀ ∃ * Queries

Uses Software

• SATCHMO
• SCOTT

Cites Work

• Proof by consistency
• Equational problems and disunification
• A method for simultaneous search for refutations and models by equational constraint solving
• Resolution methods for the decision problem
• Equational formulae with membership constraints
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Induction = I-axiomatization + first-order consistency.
• Decision procedures and model building in equational clause logic
• A transformational approach to negation in logic programming
• Hyperresolution and automated model building
• Hyper tableaux
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model building with ordered resolution: Extracting models from saturated clause sets