LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
From MaRDI portal
Publication:1111776
DOI10.1016/0020-0190(88)90124-XzbMath0658.68110OpenAlexW2079107830MaRDI QIDQ1111776
Publication date: 1988
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0020-0190(88)90124-x
Related Items
On Tackling Explanation Redundancy in Decision Trees, Properties of SLUR Formulae, Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing, SAT-Based Horn Least Upper Bounds, The unique Horn-satisfiability problem and quadratic Boolean equations., Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR, Polynomial-time inference of all valid implications for Horn and related formulae, Branch-and-cut solution of inference problems in propositional logic, Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems, Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing, Maintenance goals of agents in a dynamic environment: formulation and policy construction, A decomposition method for CNF minimality proofs, Abstract Hilbertian deductive systems, infon logic, and Datalog, A CNF Class Generalizing Exact Linear Formulas, Semantics and complexity of abduction from default theories, Hydras: complexity on general graphs and a subclass of trees, About some UP-based polynomial fragments of SAT, Horn functions and their DNFs, On the complexity of propositional knowledge base revision, updates, and counterfactuals, Hardness results for approximate pure Horn CNF formulae minimization, A subclass of Horn CNFs optimally compressible in polynomial time, Logic, Languages, and Rules for Web Data Extraction and Reasoning over Data, TRANSITIVE PRIMAL INFON LOGIC, Generalized domination in closure systems, Bounded treewidth as a key to tractability of knowledge representation and reasoning, Satisfiability of mixed Horn formulas, Recognizing renamable generalized propositional Horn formulas is NP- complete, BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies, From simplification to a partial theory solver for non-linear real polynomial constraints, Ltur, Sorting, linear time and the satisfiability problem, Efficient Reasoning for Inconsistent Horn Formulae, Efficient inclusion checking for deterministic tree automata and XML schemas, Recognition and dualization of disguised bidual Horn functions., A variant of Reiter's hitting-set algorithm, On functional dependencies in \(q\)-Horn theories
Uses Software
Cites Work
- A switching algorithm for the solution of quadratic Boolean equations
- Complete problems for deterministic polynomial time
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- HORNLOG: A graph-based interpreter for general Horn clauses
- On the Complexity of Timetable and Multicommodity Flow Problems
- The complexity of theorem-proving procedures
- Unnamed Item
- Unnamed Item
- Unnamed Item
