Implication of clauses is undecidable

DOI10.1016/0304-3975(88)90146-6zbMath0657.03006OpenAlexW2038745317MaRDI QIDQ1110493

Manfred Schmidt-Schauss

Publication date: 1988

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(88)90146-6

zbMATH Keywords

decision problemsautomated deduction systemsimplication of clauses

Mathematics Subject Classification ID

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

Related Items

Satisfiability of the smallest binary program, Quantifier-Free Equational Logic and Prime Implicate Generation, Reduction of cycle unification of type \(Cpg+r\), Computing answers with model elimination, Logical reduction of metarules, Removing redundancy from a clause, On the complexity of entailment in existential conjunctive first-order logic with atomic negation, Towards an algorithmic construction of cut-elimination procedures, Primal grammars and unification modulo a binary clause, Thue trees

Cites Work

• Properties of substitutions and unifications
• Subsumption and implication
• Solvable cases of the decision problem
• Z-Resolution: Theorem-Proving with Compiled Axioms
• The unsolvability of the Gödel class with identity
• The decision problem for formulas with a small number of atomic subformulas
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item