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-XzbMATH Open0658.68110OpenAlexW2079107830MaRDI QIDQ1111776FDOQ1111776
Authors: Michel Minoux 
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
Recommendations
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Algorithms for testing the satisfiability of propositional formulae
- Recognition of \(q\)-Horn formulae in linear time
- A note on Dowling and Gallier's top-down algorithm for propositional Horn satisfiability
- Extended Horn sets in propositional logic
Cites Work
- HORNLOG: A graph-based interpreter for general Horn clauses
- Title not available (Why is that?)
- The complexity of theorem-proving procedures
- On the Complexity of Timetable and Multicommodity Flow Problems
- Complete problems for deterministic polynomial time
- Title not available (Why is that?)
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Title not available (Why is that?)
- A switching algorithm for the solution of quadratic Boolean equations
Cited In (41)
- A decomposition method for CNF minimality proofs
- Abstract Hilbertian deductive systems, infon logic, and Datalog
- A CNF Class Generalizing Exact Linear Formulas
- Bounded treewidth as a key to tractability of knowledge representation and reasoning
- Recognizing renamable generalized propositional Horn formulas is NP- complete
- Satisfiability of mixed Horn formulas
- A subclass of Horn CNFs optimally compressible in polynomial time
- The unique Horn-satisfiability problem and quadratic Boolean equations.
- On the complexity of propositional knowledge base revision, updates, and counterfactuals
- Efficient inclusion checking for deterministic tree automata and XML schemas
- Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR
- Horn functions and their DNFs
- Copy complexity of Horn formulas with respect to unit read-once resolution
- Unique satisfiability of Horn sets can be solved in nearly linear time
- BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies
- Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
- Polynomial-time inference of all valid implications for Horn and related formulae
- On functional dependencies in \(q\)-Horn theories
- On Tackling Explanation Redundancy in Decision Trees
- Properties of SLUR Formulae
- Hardness results for approximate pure Horn CNF formulae minimization
- Maintenance goals of agents in a dynamic environment: formulation and policy construction
- A note on Dowling and Gallier's top-down algorithm for propositional Horn satisfiability
- Generalized domination in closure systems
- Branch-and-cut solution of inference problems in propositional logic
- Ltur
- A variant of Reiter's hitting-set algorithm
- Extended Horn sets in propositional logic
- Sorting, linear time and the satisfiability problem
- Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Efficient reasoning for inconsistent Horn formulae
- Semantics and complexity of abduction from default theories
- Transitive primal infon logic
- SAT-Based Horn Least Upper Bounds
- Hydras: complexity on general graphs and a subclass of trees
- About some UP-based polynomial fragments of SAT
- From simplification to a partial theory solver for non-linear real polynomial constraints
- Logic, languages, and rules for web data extraction and reasoning over data
- Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing
- Recognition and dualization of disguised bidual Horn functions.
Uses Software
This page was built for publication: LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1111776)
