Representing and building models for decidable subclasses of equational clausal logic

DOI10.1007/s10817-004-5555-7zbMath1105.03017OpenAlexW1968211553MaRDI QIDQ861367

Nicolas Peltier

Publication date: 29 January 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-004-5555-7

zbMATH Keywords

model buildingresolutiondecision proceduremodel representation

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (1)

Extracting models from clause sets saturated under semantic refinements of the resolution rule.

Uses Software

• SPASS
• SATCHMO

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
• Unnamed Item
• Complete axiomatizations of some quotient term algebras
• Resolution methods for the decision problem
• On the duality of abduction and model generation in a framework for model generation with equality
• Equational formulae with membership constraints
• Model building with ordered resolution: Extracting models from saturated clause sets
• A calculus combining resolution and enumeration for building finite models
• Hyperresolution for guarded formulae
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Using resolution for testing modal satisfiability and building models
• SHR Tableaux -- A Framework for Automated Model Generation
• On the decidability of the PVD class with equality
• Hyper Tableaux with Equality
• An Efficient Unification Algorithm
• Resolution Strategies as Decision Procedures
• Proving refutational completeness of theorem-proving strategies
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Decision procedures and model building in equational clause logic
• Hyperresolution and automated model building
• A Resolution-based Model Building Algorithm for a Fragment of OCC1N =
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution

This page was built for publication: Representing and building models for decidable subclasses of equational clausal logic