BDI: a new decidable clause class

DOI10.1093/logcom/exu074zbMath1444.03015OpenAlexW2065145482MaRDI QIDQ2987061

Christoph Weidenbach, Manuel Lamotte-Schubert

Publication date: 17 May 2017

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exu074

zbMATH Keywords

first-order logicresolutiondecidable fragmentsdecidable clause classes

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (4)

Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ \(Log_A\mathbf{G}\): an algebraic non-monotonic logic for reasoning with graded propositions ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ SGGS decision procedures

This page was built for publication: BDI: a new decidable clause class