Implication of clauses is undecidable
From MaRDI portal
Publication:1110493
DOI10.1016/0304-3975(88)90146-6zbMATH Open0657.03006OpenAlexW2038745317MaRDI QIDQ1110493FDOQ1110493
Authors: Manfred Schmidt-Schauß 
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
Recommendations
- scientific article; zbMATH DE number 1256672
- The Implication Problem for Functional and Inclusion Dependencies is Undecidable
- scientific article; zbMATH DE number 1555187
- The undecidability of entailment and relevant implication
- Undecidable problems for propositional calculi with implication
- An unsolvable problem concerning implicational calculi.
- Undecidability of the problem of recognizing axiomatizations for propositional calculi with implication
- scientific article; zbMATH DE number 517063
- scientific article; zbMATH DE number 861626
- Undecidable iterative propositional calculus
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Undecidability and degrees of sets of sentences (03D35)
Cites Work
- Title not available (Why is that?)
- A Machine-Oriented Logic Based on the Resolution Principle
- Properties of substitutions and unifications
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The unsolvability of the Gödel class with identity
- Title not available (Why is that?)
- Solvable cases of the decision problem
- Subsumption and implication
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Z-Resolution: Theorem-Proving with Compiled Axioms
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The decision problem for formulas with a small number of atomic subformulas
Cited In (12)
- Reduction of cycle unification of type \(Cpg+r\)
- Removing redundancy from a clause
- On the complexity of entailment in existential conjunctive first-order logic with atomic negation
- Satisfiability of the smallest binary program
- Towards an algorithmic construction of cut-elimination procedures
- Computing answers with model elimination
- Title not available (Why is that?)
- Thue trees
- Logical reduction of metarules
- Primal grammars and unification modulo a binary clause
- Quantifier-free equational logic and prime implicate generation
- Title not available (Why is that?)
This page was built for publication: Implication of clauses is undecidable
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1110493)
