scientific article; zbMATH DE number 3568056

Cited in

(only showing first 100 items - show all)

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
Near-Horn Prolog and the ancestry family of procedures
Formalizing incomplete knowledge in incomplete databases
\(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\)
A new algorithm for the propositional satisfiability problem
A new subsumption method in the connection graph proof procedure
ABox abduction in the description logic \(\mathcal{ALC}\)
Automatic verification of cryptographic protocols with SETHEO
Theorem proving by chain resolution
Semi-intelligible Isar proofs from machine-generated proofs
Exact knowledge compilation in predicate calculus: the partial achievement case
Linear resolution for consequence finding
A note on the completeness of resolution without self-resolution
A hierarchy of propositional Horn formuls
The search efficiency of theorem proving strategies
Answering atomic queries in indefinite deductive databases
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.
A theorem prover for a computational logic
Local simplification
Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
Theorem-proving with resolution and superposition
An algorithm for the retrieval of unifiers from discrimination trees
What you always wanted to know about rigid \(E\)-unification
Branching rules for satisfiability
SiCoTHEO: Simple competitive parallel theorem provers
Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
Complexity of resolution proofs and function introduction
A weight-balanced branching rule for SAT
Unification in a combination of arbitrary disjoint equational theories
Generalized subsumption and its applications to induction and redundancy
An efficient algorithm for the 3-satisfiability problem
\(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description
Defining answer classes using resolution refutation
Solving propositional satisfiability problems
Hierarchical deduction
First order LUB approximations: characterization and algorithms
Partition-based logical reasoning for first-order and propositional theories
Unification theory
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
A Prolog technology theorem prover: A new exposition and implementation in Prolog
Uniform and non uniform strategies for tableaux calculi for modal logics
Tractable reasoning via approximation
Computing answers with model elimination
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.
An extension to linear resolution with selection function
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
HyperMonitor: a Python prototype for hyper predictive runtime verification
Knowledge-based proof planning
How good are branching rules in DPLL?
Branch-and-cut solution of inference problems in propositional logic
Logic applied to integer programming and integer programming applied to logic

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)