scientific article; zbMATH DE number 3568056

Cited in

(only showing first 100 items - show all)

The Multi-SAT algorithm
An automatic proof of Gödel's incompleteness theorem
A new method for knowledge compilation: The achievement by cycle search
Combining instance generation and resolution
On the mechanical derivation of loop invariants
Subsumption-linear Q-resolution for QBF theorem proving
Negation as failure: careful closure procedure
Craig interpolation with clausal first-order tableaux
A practically efficient and almost linear unification algorithm
Efficient solution of linear diophantine equations
Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae
A simplified problem reduction format
TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic
On subsumption in distributed derivations
Problem solving by searching for models with a theorem prover
Exact Max-SAT solvers for over-constrained problems
Recursive query processing: The power of logic
A complete adaptive algorithm for propositional satisfiability
Prolog technology for default reasoning: proof theory and compilation techniques
Reduction rules for resolution-based systems
Approximating minimal unsatisfiable subformulae by means of adaptive core search
A utility-valued logic for decision making
Automated deduction with associative-commutative operators
Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
An efficient solver for weighted Max-SAT
Term rewriting: Some experimental results
Partheo: A high-performance parallel theorem prover
History and basic features of the critical-pair/completion procedure
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
A method for simultaneous search for refutations and models by equational constraint solving
Subgoal alternation in model elimination
Modeling production rules by means of predicate transition networks
A resolution principle for constrained logics
Investigations into proof structures
Verifying local stratifiability of logic programs and databases
Connection tableaux with lazy paramodulation
Semantic tableaux with ordering restrictions
A parallel approach for theorem proving in propositional logic
Controlled use of clausal lemmas in connection tableau calculi
Subsumption and implication
A comparative study of several proof procedures
1998–99 Annual Meeting of the Association for Symbolic Logic
scientific article; zbMATH DE number 7680806 (Why is no real title available?)
The applicability of logic program analysis and transformation to theorem proving
Linear strategy for Boolean ring based theorem proving
Meta-resolution: An algorithmic formalisation
Lemmas: generation, selection, application
Range-restricted and Horn interpolation through clausal tableaux
Simplifying clausal satisfiability problems
Mode-Directed Inverse Entailment for Full Clausal Theories
Connection calculus theorem proving with multiple built-in theories
Hierarchies of polynomially solvable satisfiability problems
A relevance restriction strategy for automated deduction
A general framework to build contextual cover set induction provers
The practicality of generating semantic trees for proofs of unsatisfiability
Linear and unit-resulting refutations for Horn theories
Learning action models from plan examples using weighted MAX-SAT
Using forcing to prove completeness of resolution and paramodulation
Closures and fairness in the semantics of programming logic
Semantics of Horn and disjunctive logic programs
Propositional calculus problems in CHIP
Gentzen-type systems, resolution and tableaux
Building Theorem Provers
Backtracking tactics in the backtrack method for SAT
A note on assumptions about Skolem functions
An order-sorted logic for knowledge representation systems
An implementation of Kripke-Kleene semantics
Book review of: S. Russell and P. Norvig, Artificial intelligence: a modern approach
Parsing as non-Horn deduction
Compiling a default reasoning system into Prolog
Set of support, demodulation, paramodulation: a historical perspective
A superposition oriented theorem prover
Link inheritance in abstract clause graphs
Man-machine theorem proving in graph theory
Generalized conflict-clause strengthening for satisfiability solvers
Strategies for modal resolution: Results and problems
Extracting models from clause sets saturated under semantic refinements of the resolution rule.
Removing redundancy from a clause
Producing and verifying extremely large propositional refutations
A classification of non-liftable orders for resolution
Lemma matching for a PTTP-based top-down theorem prover
Building proofs or counterexamples by analogy in a resolution framework
Case-free programs: An abstraction of definite horn programs
The approximation of implicates and explanations
On preprocessing techniques and their impact on propositional model counting
Implication of clauses is undecidable
Goal directed strategies for paramodulation
\(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
Embedding circumscriptive theories in general disjunctive programs
Fuzzy logic programming
Linear programs for constraint satisfaction problems
SATCHMORE: SATCHMO with RElevancy
Linearity and regularity with negation normal form
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
Semantic trees revisited: some new completeness results
Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
Local simplification
Clause trees: A tool for understanding and implementing resolution in automated reasoning
A structure-preserving clause form translation
Avoiding duplicate proofs with the foothold refinement

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)