scientific article; zbMATH DE number 3254919

Cited in

(64)

Completeness of hyper-resolution via the semantics of disjunctive logic programs
Complete problems in the first-order predicate calculus
Theorem proving with abstraction
Lower bounds for increasing complexity of derivations after cut elimination
The Earley algorithm as a problem representation
Experimental tests of resolution-based theorem-proving strategies
An implementation of hyper-resolution
Analytic resolution in theorem proving
Mechanizing $\omega$-order type theory through unification
Metamathematical approach to proving theorems of discrete mathematics
Basic research problems: The problem of strategy and hyperresolution
The rue theorem-proving system: The complete set of LIM+ challenge problems
The problem of hyperparamodulation
Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
The application of automated reasoning to questions in mathematics and logic
Hyperresolution for guarded formulae
A new fuzzy resolution principle based on the antonym
Semantically-guided goal-sensitive reasoning: inference system and completeness
Presenting inequations in mathematical proofs
The application of automated reasoning to formal models of combinatorial optimization
The anatomy of vampire. Implementing bottom-up procedures with code trees
Jean van Heijenoort's contributions to proof theory and its history
Larry Wos: visions of automated reasoning
Set of support, demodulation, paramodulation: a historical perspective
Contradiction separation based dynamic multi-clause synergized automated deduction
Blocking and other enhancements for bottom-up model generation methods
$\mathrm{K}_{\mathrm S}\mathrm{P}$ a resolution-based theorem prover for ${\mathsf{K}}_n$: architecture, refinements, strategies and experiments
Hyperresolution for Gödel logic with truth constants
Finding resolution proofs and using duplicate goals in AND/OR trees
Theorem proving with variable-constrained resolution
Beweisalgorithmen für die Prädikatenlogik
The application of the methods of the theory of logical derivation to graph theory
Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies
Labelled interpolation systems for hyper-resolution, clausal, and local proofs
Semantically-guided goal-sensitive reasoning: model representation
On First-Order Model-Based Reasoning
History and prospects for first-order automated deduction
A Modal-Layered Resolution Calculus for K
Semantical Completeness Theorems in Logic and Algebra
On deciding satisfiability by theorem proving with speculative inferences
Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable
Tableaux for diagnosis applications
Minimal model generation with positive unit hyper-resolution tableaux
Advanced indexing operations on substitution trees
MRPPS?An interactive refutation proof procedure system for question-answering
A resolution-based model building algorithm for a fragment of $\mathcal{OCC}1\mathcal{N}_{=}$ (extended abstract)
Linking focusing and resolution with selection
The search efficiency of theorem proving strategies
Hyper tableaux
An algorithm for the retrieval of unifiers from discrimination trees
Theorem proving techniques for view deletion in databases
A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
On structures of regular standard contradictions in propositional logic
Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
Classical algorithms for reasoning and explanation in description logics
Range-restricted and Horn interpolation through clausal tableaux
Parsing as non-Horn deduction
Model construction for modal clauses
Basic research problems: The problem of choosing the representation, inference rule, and strategy
The problem of choosing the type of subsumption to use
Some techniques for proving termination of the hyperresolution calculus
Steps toward a computational metaphysics
Completeness of resolution revisited

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 Q5541351)