Extending decidable clause classes via constraints

DOI10.1007/3-540-46508-1_14MaRDI QIDQ4503912zbMATH OpenFDO

Authors Reinhard Pichler

Publication date 14 September 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46508-1_14

zbMATH Keywords

compactnessconstrained clause logicresolution-based decision proceduresunification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Reasoning on constraints in CLP(FD)
• scientific article; zbMATH DE number 7680806
• Solving constrained Horn clauses using dependence-disjoint expansions
• Approximability of clausal constraints
• Complexity of clausal constraints over chains
• BDI: a new decidable clause class
• Completeness and redundancy in constrained clause logic
• Representing and building models for decidable subclasses of equational clausal logic
• scientific article; zbMATH DE number 2040978
• scientific article; zbMATH DE number 7713505

Cited in

(10)

• A resolution principle for a logic with restricted quantifiers
• Extending H₁-clauses with disequalities
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Extending \({\mathcal H}_1\)-clauses with path disequalities
• Crossing the syntactic barrier: hom-disequalities for \({\mathcal H}_1\)-clauses
• BDI: a new decidable clause class
• scientific article; zbMATH DE number 516985 (Why is no real title available?)
• scientific article; zbMATH DE number 516992 (Why is no real title available?)
• Completeness and redundancy in constrained clause logic
• scientific article; zbMATH DE number 7680806 (Why is no real title available?)

This page was built for publication: Extending decidable clause classes via constraints

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