scientific article; zbMATH DE number 3568056
From MaRDI portal
Publication:4139711
zbMATH Open0364.68082MaRDI QIDQ4139711FDOQ4139711
Authors: Donald W. Loveland 
Publication date: 1978
Title of this publication is not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Closures and fairness in the semantics of programming logic
- Gentzen-type systems, resolution and tableaux
- Semantics of Horn and disjunctive logic programs
- An order-sorted logic for knowledge representation systems
- An implementation of Kripke-Kleene semantics
- Parsing as non-Horn deduction
- A superposition oriented theorem prover
- Compiling a default reasoning system into Prolog
- Strategies for modal resolution: Results and problems
- Removing redundancy from a clause
- Producing and verifying extremely large propositional refutations
- Goal directed strategies for paramodulation
- Fuzzy logic programming
- Implication of clauses is undecidable
- Embedding circumscriptive theories in general disjunctive programs
- SATCHMORE: SATCHMO with RElevancy
- Linear programs for constraint satisfaction problems
- Linearity and regularity with negation normal form
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\)
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- A structure-preserving clause form translation
- A new algorithm for the propositional satisfiability problem
- The search efficiency of theorem proving strategies
- Linear resolution for consequence finding
- Semi-intelligible Isar proofs from machine-generated proofs
- Representing and building models for decidable subclasses of equational clausal logic
- Some techniques for proving termination of the hyperresolution calculus
- The achievement of knowledge bases by cycle search.
- Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
- Branching rules for satisfiability
- Theorem-proving with resolution and superposition
- Complexity of resolution proofs and function introduction
- Generalized subsumption and its applications to induction and redundancy
- A weight-balanced branching rule for SAT
- Unification in a combination of arbitrary disjoint equational theories
- An efficient algorithm for the 3-satisfiability problem
- Defining answer classes using resolution refutation
- First order LUB approximations: characterization and algorithms
- Partition-based logical reasoning for first-order and propositional theories
- Solving propositional satisfiability problems
- Hierarchical deduction
- Unification theory
- Uniform and non uniform strategies for tableaux calculi for modal logics
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A Noetherian and confluent rewrite system for idempotent semigroups
- About the Paterson-Wegman linear unification algorithm
- Tractable reasoning via approximation
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Some results and experiments in programming techniques for propositional logic
- Resolution vs. cutting plane solution of inference problems: Some computational experience
- Embedding complex decision procedures inside an interactive theorem prover.
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- Controlled integration of the cut rule into connection tableau calculi
- Knowledge-based proof planning
- How good are branching rules in DPLL?
- Branch-and-cut solution of inference problems in propositional logic
- The \(Multi\)-SAT algorithm
- Combining instance generation and resolution
- Logic applied to integer programming and integer programming applied to logic
- Negation as failure: careful closure procedure
- A practically efficient and almost linear unification algorithm
- Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
- Efficient solution of linear diophantine equations
- Exact Max-SAT solvers for over-constrained problems
- A simplified problem reduction format
- Recursive query processing: The power of logic
- Prolog technology for default reasoning: proof theory and compilation techniques
- Approximating minimal unsatisfiable subformulae by means of adaptive core search
- A utility-valued logic for decision making
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification
- An efficient solver for weighted Max-SAT
- Term rewriting: Some experimental results
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- A parallel approach for theorem proving in propositional logic
- Title not available (Why is that?)
- Subsumption and implication
- Mode-Directed Inverse Entailment for Full Clausal Theories
- Meta-resolution: An algorithmic formalisation
- A general framework to build contextual cover set induction provers
- A relevance restriction strategy for automated deduction
- Learning action models from plan examples using weighted MAX-SAT
- Using forcing to prove completeness of resolution and paramodulation
- Propositional calculus problems in CHIP
- Building Theorem Provers
- A note on assumptions about Skolem functions
- Backtracking tactics in the backtrack method for SAT
- Book review of: S. Russell and P. Norvig, Artificial intelligence: a modern approach
- Set of support, demodulation, paramodulation: a historical perspective
- Generalized conflict-clause strengthening for satisfiability solvers
- Link inheritance in abstract clause graphs
- Case-free programs: An abstraction of definite horn programs
- Man-machine theorem proving in graph theory
- A classification of non-liftable orders for resolution
- Lemma matching for a PTTP-based top-down theorem prover
- What you always wanted to know about rigid E-unification
- Building proofs or counterexamples by analogy in a resolution framework
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- On preprocessing techniques and their impact on propositional model counting
- The approximation of implicates and explanations
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4139711)
