BDI: a new decidable clause class

DOI10.1093/LOGCOM/EXU074MaRDI QIDQ2987061zbMATH OpenOpenAlexFDO

Authors Manuel Lamotte-Schubert, Christoph Weidenbach

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

decidable clause classesdecidable fragmentsfirst-order logicresolution

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2090304
• scientific article; zbMATH DE number 512974
• Deciding H₁ by resolution
• scientific article; zbMATH DE number 1507192
• Some techniques for proving termination of the hyperresolution calculus

Cited in

(8)

• \(\mathit{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
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• scientific article; zbMATH DE number 1507192 (Why is no real title available?)
• scientific article; zbMATH DE number 2090304 (Why is no real title available?)
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• First-order automatic literal model generation

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2987061)