On generalized Horn formulas and \(k\)-resolution
From MaRDI portal
Publication:685363
DOI10.1016/0304-3975(93)90331-MzbMath0786.03009OpenAlexW1504884225MaRDI QIDQ685363
Publication date: 5 May 1994
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(93)90331-m
Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)
Related Items (9)
Generalising and Unifying SLUR and Unit-Refutation Completeness ⋮ On resolution with short clauses ⋮ Hierarchies of polynomially solvable satisfiability problems ⋮ Space characterizations of complexity measures and size-space trade-offs in propositional proof systems ⋮ Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ Special issues on The satisfiability problem (pp. 1--244) including papers from the 1st workshop on satisfiability, Certosa di Pontignano, Italy, April 29--May 3, 1996 and Boolean functions (pp. 245--479) ⋮ First order LUB approximations: characterization and algorithms ⋮ On functional dependencies in \(q\)-Horn theories ⋮ Generalising unit-refutation completeness and SLUR via nested input resolution
Cites Work
- An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences
- Polynomially solvable satisfiability problems
- The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Recognizing disguised NR(1) instances of the satisfiability problem
- The Unit Proof and the Input Proof in Theorem Proving
This page was built for publication: On generalized Horn formulas and \(k\)-resolution
