Decision procedures and model building in equational clause logic

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

zbMATH Keywords

equational reasoningfinite model propertysaturationautomated model buildingautomated deductionpositive ordered paramodulationpositive resolution

Mathematics Subject Classification ID

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