On renamable Horn and generalized Horn functions

DOI10.1007/BF01531069zbMath0878.68106OpenAlexW1970750671WikidataQ56482743 ScholiaQ56482743MaRDI QIDQ1356207

Xiaorong Sun, Collette R. Coullard, Vijaya Chandru, Miguel Montañez, Peter L. Hammer

Publication date: 14 December 1997

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01531069

zbMATH Keywords

Horn function

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Classical propositional logic (03B05)

Related Items

Recognition of \(q\)-Horn formulae in linear time, Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing, Domain permutation reduction for constraint satisfaction problems, Hierarchies of polynomially solvable satisfiability problems, Testing heuristics: We have it all wrong, Fuzzy logic programs as hypergraphs. Termination results, Maximum renamable Horn sub-CNFs, Mixed logical-linear programming, Recognition of tractable satisfiability problems through balanced polynomial representations, Unique Horn renaming and Unique 2-Satisfiability, Resolution search, Detecting embedded Horn structure in propositional logic, Recognizing renamable generalized propositional Horn formulas is NP- complete, A linear algorithm for renaming a set of clauses as a Horn set, On functional dependencies in \(q\)-Horn theories

Uses Software

• Hornlog

Cites Work

• Unnamed Item
• Unnamed Item
• An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences
• Some results and experiments in programming techniques for propositional logic
• On renaming a set of clauses as a Horn set
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Linear programming is log-space hard for P
• 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
• A note on the complexity of the satisfiability of modal Horn clauses
• HORNLOG: A graph-based interpreter for general Horn clauses
• Recognizing disguised NR(1) instances of the satisfiability problem
• Unit Refutations and Horn Sets
• Renaming a Set of Clauses as a Horn Set
• Paths, Trees, and Flowers
• Depth-First Search and Linear Graph Algorithms
• The complexity of theorem-proving procedures