Decision procedures and model building in equational clause logic
From MaRDI portal
Publication:4380444
DOI10.1093/jigpal/6.1.17zbMath0903.03010OpenAlexW1997432585MaRDI QIDQ4380444
Alexander Leitsch, Christian G. Fermüller
Publication date: 5 January 1999
Published in: Logic Journal of IGPL (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/jigpal/6.1.17
equational reasoningfinite model propertysaturationautomated model buildingautomated deductionpositive ordered paramodulationpositive resolution
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items (10)
Representing and building models for decidable subclasses of equational clausal logic ⋮ Predicting and detecting symmetries in FOL finite model search ⋮ 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 ⋮ Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ The ground-negative fragment of first-order logic is -complete
This page was built for publication: Decision procedures and model building in equational clause logic
