LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
From MaRDI portal
(Redirected from Publication:1111776)
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
- scientific article; zbMATH DE number 3988689 (Why is no real title available?)
- scientific article; zbMATH DE number 3571502 (Why is no real title available?)
- scientific article; zbMATH DE number 3449757 (Why is no real title available?)
- A switching algorithm for the solution of quadratic Boolean equations
- Complete problems for deterministic polynomial time
- HORNLOG: A graph-based interpreter for general Horn clauses
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- On the Complexity of Timetable and Multicommodity Flow Problems
- The complexity of theorem-proving procedures
Cited in
(41)- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Sorting, linear time and the satisfiability problem
- Copy complexity of Horn formulas with respect to unit read-once resolution
- Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
- Hardness results for approximate pure Horn CNF formulae minimization
- Branch-and-cut solution of inference problems in propositional logic
- A decomposition method for CNF minimality proofs
- Abstract Hilbertian deductive systems, infon logic, and Datalog
- On the complexity of propositional knowledge base revision, updates, and counterfactuals
- Transitive primal infon logic
- Polynomial-time inference of all valid implications for Horn and related formulae
- A subclass of Horn CNFs optimally compressible in polynomial time
- Semantics and complexity of abduction from default theories
- SAT-Based Horn Least Upper Bounds
- A CNF Class Generalizing Exact Linear Formulas
- Unique satisfiability of Horn sets can be solved in nearly linear time
- Bounded treewidth as a key to tractability of knowledge representation and reasoning
- Generalized domination in closure systems
- On functional dependencies in \(q\)-Horn theories
- Properties of SLUR Formulae
- Ltur
- Extended Horn sets in propositional logic
- Efficient inclusion checking for deterministic tree automata and XML schemas
- 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
- On Tackling Explanation Redundancy in Decision Trees
- A variant of Reiter's hitting-set algorithm
- Horn functions and their DNFs
- Efficient reasoning for inconsistent Horn formulae
- Satisfiability of mixed Horn formulas
- Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR
- Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems
- Hydras: complexity on general graphs and a subclass of trees
- BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies
- From simplification to a partial theory solver for non-linear real polynomial constraints
- About some UP-based polynomial fragments of SAT
- Recognizing renamable generalized propositional Horn formulas is NP- complete
- The unique Horn-satisfiability problem and quadratic Boolean equations.
- Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing
- Logic, languages, and rules for web data extraction and reasoning over data
- Recognition and dualization of disguised bidual Horn functions.
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)
