Linear-time algorithms for testing the satisfiability of propositional horn formulae
From MaRDI portal
Publication:3723723
DOI10.1016/0743-1066(84)90014-1zbMath0593.68062OpenAlexW2011992362WikidataQ55966922 ScholiaQ55966922MaRDI QIDQ3723723
Jean H. Gallier, William F. Dowling
Publication date: 1984
Published in: The Journal of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0743-1066(84)90014-1
Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Related Items
The fraction of large random trees representing a given Boolean function in implicational logic, Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs, Reasoning with ordered binary decision diagrams, Properties of SLUR Formulae, Logic programs and connectionist networks, Nesting analysis of mobile ambients, Computing the least common subsumer w.r.t. a background terminology, Alternating two-way AC-tree automata, A decision method for nonmonotonic reasoning based on autoepistemic reasoning, Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing, SAT-Based Horn Least Upper Bounds, The arborescence-realization problem, Unique satisfiability of Horn sets can be solved in nearly linear time, A new algorithm for the propositional satisfiability problem, A rational reconstruction of nonmonotonic truth maintenance systems, Model-preference default theories, Counting for satisfiability by inverting resolution, 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, A new approach to hybrid probabilistic logic programs, What makes propositional abduction tractable, Maintenance goals of agents in a dynamic environment: formulation and policy construction, Top-down and Bottom-up Evaluation Procedurally Integrated, Qualitative probabilities for default reasoning, belief revision, and causal modeling, PALO: a probabilistic hill-climbing algorithm, Directed hypergraphs and Horn minimization, Complexity and undecidability results for logic programming, Complexity of computing with extended propositional logic programs, LoCo—A Logic for Configuration Problems, A Conceptual Framework for Secrecy-preserving Reasoning in Knowledge Bases, Unique key Horn functions, Analyzing read-once cutting plane proofs in Horn systems, Experimental results on the crossover point in random 3-SAT, Support set selection for abductive and default reasoning, Dual-normal logic programs – the forgotten class, Tropical Carathéodory with matroids, Tomographic reconstruction of 2-convex polyominoes using dual Horn clauses, An artificial neural network satisfiability tester, Exploiting data dependencies in many-valued logics, Unnamed Item, Maximum renamable Horn sub-CNFs, Bidual Horn functions and extensions, Two tractable subclasses of minimal unsatisfiable formulas, Recognition of tractable satisfiability problems through balanced polynomial representations, Canonical Inference for Implicational Systems, Conditional congruence closure over uninterpreted and interpreted symbols, An incremental algorithm for generating all minimal models, Copy complexity of Horn formulas with respect to unit read-once resolution, DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions, On the Implementation of Weight Constraint Rules in Conflict-Driven ASP Solvers, Canonical Ground Horn Theories, Model Checking Games, On generating all solutions of generalized satisfiability problems, Hardness results for approximate pure Horn CNF formulae minimization, Conflict-driven answer set solving: from theory to practice, Pseudo-models and propositional Horn inference, Generalized domination in closure systems, Unnamed Item, Bounded treewidth as a key to tractability of knowledge representation and reasoning, Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances, On exact selection of minimally unsatisfiable subformulae, Solving the resolution-free SAT problem by submodel propagation in linear time, Automata and Answer Set Programming, Belief revision in Horn theories, Enumerating Minimally Revised Specifications Using Dualization, Selecting and covering colored points, Gainfree Leontief substitution flow problems, Directed hypergraphs and applications, Computational Aspects of Quasi-Classical Entailment, Recognizing renamable generalized propositional Horn formulas is NP- complete, BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies, Inference approach based on Petri nets, From simplification to a partial theory solver for non-linear real polynomial constraints, Sorting, linear time and the satisfiability problem, Some (in)translatability results for normal logic programs and propositional theories, A multiparametric view on answer set programming, Efficient Reasoning for Inconsistent Horn Formulae, Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas, Multi-agent path finding with mutex propagation, On subclasses of minimal unsatisfiable formulas, Using model theory to find decidable and tractable description logics with concrete domains, The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas, Backdoors to tractable answer set programming, A short note on some tractable cases of the satisfiability problem., Efficient and flexible matching of recursive types, Tarskian set constraints, Horn approximations of empirical data, Tractable reasoning via approximation, A sharp threshold for the renameable-Horn and the \(q\)-Horn properties, Typical case complexity of satisfiability algorithms and the threshold phenomenon, Feasibility checking in Horn constraint systems through a reduction based approach, The possibilistic Horn non-clausal knowledge bases, A perspective on certain polynomial-time solvable classes of satisfiability, Ordered binary decision diagrams as knowledge-bases, Logical analysis of binary data with missing bits, On functional dependencies in \(q\)-Horn theories, The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies, Two-sided context specifications in formal grammars, Efficient all-UIP learned clause minimization, An efficient algorithm for a class of constraint satisfaction problems, Model checking and boolean graphs, Computing definite logic programs by partial instantiation, Theory refinement combining analytical and empirical methods, The complexity of propositional closed world reasoning and circumscription, The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics, Logic programming in tensor spaces, Recognition of \(q\)-Horn formulae in linear time, Limited reasoning in first-order knowledge bases, The problem of asking the minimum number of questions in Horn clause systems, On the complexity of the maximum satisfiability problem for Horn formulas, A hypergraph model for constraint logic programming and applications to bus drivers' scheduling, The unique Horn-satisfiability problem and quadratic Boolean equations., Fast algorithms for testing unsatisfiability of ground Horn clauses with equations, Polynomial-time inference of all valid implications for Horn and related formulae, On renamable Horn and generalized Horn functions, Branch-and-cut solution of inference problems in propositional logic, Solving propositional satisfiability problems, Question-asking strategies for Horn clause systems, Positive and Horn decomposability of partially defined Boolean functions, Possibilistic uncertainty handling for answer set programming, Answer set programming based on propositional satisfiability, LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation, Polynomially solvable satisfiability problems, Optimizing propositional calculus formulas with regard to questions of deducibility, Stratification and knowledge base management, On resolution with short clauses, Unification in sort theories and its applications, On computing minimal models, On the complexity of entailment in propositional multivalued logics, Hierarchies of polynomially solvable satisfiability problems, A cost effective question-asking strategy for Horn clause systems, A fast parallel SAT-solver -- efficient workload balancing, Max Horn SAT and the minimum cut problem in directed hypergraphs, Reasoning with minimal models: efficient algorithms and applications, Relevance from an epistemic perspective, A decomposition method for CNF minimality proofs, Revision programming, Abstract Hilbertian deductive systems, infon logic, and Datalog, Is intractability of nonmonotonic reasoning a real drawback?, Reducing belief revision to circumscription (and vice versa), On the complexity of enumerating pseudo-intents, Information-based distance measures and the canonical reflection of view updates, Dynamic maintenance of directed hypergraphs, Existence of simple propositional formulas, Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search, Colouring, constraint satisfaction, and complexity, Guarantees and limits of preprocessing in constraint satisfaction and reasoning, Disjunctive closures for knowledge compilation, An efficient automata approach to some problems on context-free grammars., Generalising submodularity and Horn clauses: Tractable optimization problems defined by tournament pair multimorphisms, Hard problems for simple default logics, On the tractability of minimal model computation for some CNF theories, Models and quantifier elimination for quantified Horn formulas, Unique Horn renaming and Unique 2-Satisfiability, On the consistency of defeasible databases, Directed hypergraphs: introduction and fundamental algorithms -- a survey, Succinctness and tractability of closure operator representations, Learning definite Horn formulas from closure queries, Hydras: complexity on general graphs and a subclass of trees, Capturing complexity classes by fragments of second-order logic, Constraint acquisition, About some UP-based polynomial fragments of SAT, Horn functions and their DNFs, Detecting embedded Horn structure in propositional logic, Skeptical reason maintenance and belief revision, On generalized Horn formulas and \(k\)-resolution, On the complexity of propositional knowledge base revision, updates, and counterfactuals, Sensitivity analysis for Horn formulae, An efficient algorithm for the 3-satisfiability problem, Complexity of unification problems with associative-commutative operators, The logic of constraint satisfaction, Structure identification in relational data, A subclass of Horn CNFs optimally compressible in polynomial time, A hierarchy of tractable satisfiability problems, Incremental classification of description logics ontologies, Complexity of pairwise shortest path routing in the grid, Decidable containment of recursive queries, A dual algorithm for the satisfiability problem, Negation in rule-based database languages: A survey, Negation by default and unstratifiable logic programs, Algorithms for the maximum satisfiability problem, Local simplification, Double Horn functions, Inheritance comes of age: applying nonmonotonic techniques to problems in industry, On the relation among answer set solvers, Armstrong axioms and Boyce-Codd-Heath normal form under bag semantics, Semantical and computational aspects of Horn approximations, Logic programs, well-orderings, and forward chaining, Compact and efficient encodings for planning in factored state and action spaces with learned binarized neural network transition models, Conjunctive-query containment and constraint satisfaction, A linear time algorithm for unique Horn satisfiability, Optimal compression of propositional Horn knowledge bases: Complexity and approximation, Validating firewalls using flow logics, Extending and implementing the stable model semantics, A linear algorithm for renaming a set of clauses as a Horn set, Inference flexibility in Horn clause knowledge bases and the simplex method, Cyclic consistency: A local reduction operation for binary valued constraints, Theory revision with queries: Horn, read-once, and parity formulas, Multi-modal diagnosis combining case-based and model-based reasoning: a formal and experimental analysis, An NSF proposal, Backdoors to Normality for Disjunctive Logic Programs, Witnesses for Answer Sets of Logic Programs, Modular Inference of Linear Types for Multiplicity-Annotated Arrows, Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR, Propositional calculus problems in CHIP, Merging heterogeneous security orderings, Computing the well-founded semantics faster, A Survey of the Proof-Theoretic Foundations of Logic Programming, The number of satisfying assignments of random 2‐SAT formulas, Fuzzy logic programs as hypergraphs. Termination results, A first polynomial non-clausal class in many-valued logic, SAT backdoors: depth beats size, Unnamed Item, Extensions of unification modulo ACUI, Finding Effective SAT Partitionings Via Black-Box Optimization, On the difference of Horn theories, TRANSITIVE PRIMAL INFON LOGIC, Tractable constraints in finite semilattices, Acquiring Generalized Domain-Range Restrictions, Decision lists and related Boolean functions, Rethinking Defeasible Reasoning: A Scalable Approach, Unnamed Item, Using Merging Variables-Based Local Search to Solve Special Variants of MaxSAT Problem, Towards the Use of Hypergraphs in Multi-adjoint Logic Programming, Convex Aggregation Problems in $$\mathbb {Z}^2$$, Semantic Bijectivity and the Uniqueness of Constant-Complement Updates in the Relational Context, Approximating Minimum Representations of Key Horn Functions, Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals
