scientific article; zbMATH DE number 3568056

Cited in

(only showing first 100 items - show all)

Learning action models from plan examples using weighted MAX-SAT
Modeling production rules by means of predicate transition networks
A superposition oriented theorem prover
Subsumption and implication
Link inheritance in abstract clause graphs
Negation as failure: careful closure procedure
A structure-preserving clause form translation
Hierarchical deduction
Resolution vs. cutting plane solution of inference problems: Some computational experience
Some results and experiments in programming techniques for propositional logic
A parallel approach for theorem proving in propositional logic
History and basic features of the critical-pair/completion procedure
About the Paterson-Wegman linear unification algorithm
Man-machine theorem proving in graph theory
A practically efficient and almost linear unification algorithm
Generalized subsumption and its applications to induction and redundancy
Implication of clauses is undecidable
A Prolog technology theorem prover: Implementation by an extended Prolog compiler
A note on the completeness of resolution without self-resolution
Efficient solution of linear diophantine equations
A hierarchy of propositional Horn formuls
Unification theory
Logic applied to integer programming and integer programming applied to logic
An extension to linear resolution with selection function
A Noetherian and confluent rewrite system for idempotent semigroups
A simplified problem reduction format
Semantics of Horn and disjunctive logic programs
Reduction rules for resolution-based systems
An order-sorted logic for knowledge representation systems
Complexity of resolution proofs and function introduction
A method for simultaneous search for refutations and models by equational constraint solving
A new subsumption method in the connection graph proof procedure
Linear resolution for consequence finding
A Prolog technology theorem prover: A new exposition and implementation in Prolog
An efficient algorithm for the 3-satisfiability problem
Verifying local stratifiability of logic programs and databases
Recursive query processing: The power of logic
Local simplification
Theorem proving by chain resolution
Prolog technology for default reasoning: proof theory and compilation techniques
Linear programs for constraint satisfaction problems
How good are branching rules in DPLL?
An implementation of Kripke-Kleene semantics
The approximation of implicates and explanations
Gentzen-type systems, resolution and tableaux
On the mechanical derivation of loop invariants
A resolution principle for constrained logics
TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic
On subsumption in distributed derivations
Formalizing incomplete knowledge in incomplete databases
Problem solving by searching for models with a theorem prover
Automated deduction with associative-commutative operators
Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
Controlled integration of the cut rule into connection tableau calculi
Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
Embedding complex decision procedures inside an interactive theorem prover.
Branch-and-cut solution of inference problems in propositional logic
Solving propositional satisfiability problems
Hierarchies of polynomially solvable satisfiability problems
Extracting models from clause sets saturated under semantic refinements of the resolution rule.
Clause trees: A tool for understanding and implementing resolution in automated reasoning
Computing answers with model elimination
Approximating minimal unsatisfiable subformulae by means of adaptive core search
\(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
Linear strategy for Boolean ring based theorem proving
Backtracking tactics in the backtrack method for SAT
A complete adaptive algorithm for propositional satisfiability
A comparative study of several proof procedures
The achievement of knowledge bases by cycle search.
Tractable reasoning via approximation
SATCHMORE: SATCHMO with RElevancy
A new algorithm for the propositional satisfiability problem
Branching rules for satisfiability
A note on assumptions about Skolem functions
Linear and unit-resulting refutations for Horn theories
Near-Horn Prolog and the ancestry family of procedures
Avoiding duplicate proofs with the foothold refinement
The Multi-SAT algorithm
Knowledge-based proof planning
Set of support, demodulation, paramodulation: a historical perspective
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
On preprocessing techniques and their impact on propositional model counting
ABox abduction in the description logic \(\mathcal{ALC}\)
First order LUB approximations: characterization and algorithms
Partition-based logical reasoning for first-order and propositional theories
Exact Max-SAT solvers for over-constrained problems
Craig interpolation with clausal first-order tableaux
Book review of: S. Russell and P. Norvig, Artificial intelligence: a modern approach
The practicality of generating semantic trees for proofs of unsatisfiability
Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
Semi-intelligible Isar proofs from machine-generated proofs
Generalized conflict-clause strengthening for satisfiability solvers
Answering atomic queries in indefinite deductive databases
Combining instance generation and resolution
Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
Subgoal alternation in model elimination
Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
SiCoTHEO: Simple competitive parallel theorem provers
\(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description

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)