On the decidability of the PVD class with equality

DOI10.1093/jigpal/9.4.569zbMath0980.03012OpenAlexW1973424310MaRDI QIDQ2743641

Nicolas Peltier

Publication date: 12 March 2002

Published in: Logic Journal of IGPL (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/jigpal/9.4.569

zbMATH Keywords

model buildingdecidabilityautomated deductiondecision proceduresPVDresolution refinementsimultaneous ordered paramodulation

Mathematics Subject Classification ID

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

Related Items (2)

Representing and building models for decidable subclasses of equational clausal logic ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).

This page was built for publication: On the decidability of the PVD class with equality