Automatic Theorem Proving With Renamable and Semantic Resolution
From MaRDI portal
Cited in
(41)- Saturation, nonmonotonic reasoning and the closed-world assumption
- One modification of the ordering strategy in the resolution method
- Theorem proving with abstraction
- A semantic backward chaining proof system
- A method for simultaneous search for refutations and models by equational constraint solving
- Non-resolution theorem proving
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- The Q^* algorithm - a search strategy for a deductive question-answering system
- Solving SAT by algorithm transform of Wu's method
- Separable resolution method for checking the satisfiability of formulas in the language \({\mathfrak L}\)
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Renamable paramodulation for automatic theorem proving with equality
- Resolution graphs
- Finding resolution proofs and using duplicate goals in AND/OR trees
- Theorem proving with variable-constrained resolution
- A note on linear resolution strategies in consequence-finding
- Semantically-guided goal-sensitive reasoning: model representation
- On First-Order Model-Based Reasoning
- Multi-ary \(\alpha\)-semantic resolution automated reasoning based on lattice-valued first-order logic \(\mathrm{LF}(X)\)
- Combining instance generation and resolution
- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
- Semantic trees revisited: some new completeness results
- MRPPS?An interactive refutation proof procedure system for question-answering
- Linking focusing and resolution with selection
- The search efficiency of theorem proving strategies
- A method for building models automatically. Experiments with an extension of OTTER
- Semantic tableaux with ordering restrictions
- Soft typing for ordered resolution
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- On structures of regular standard contradictions in propositional logic
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- A complete semantic back chaining proof system
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
- Range-restricted and Horn interpolation through clausal tableaux
- Decision procedures using model building techniques
- Parsing as non-Horn deduction
- Model construction for modal clauses
- Representing and building models for decidable subclasses of equational clausal logic
- Completeness of resolution revisited
This page was built for publication: Automatic Theorem Proving With Renamable and Semantic Resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5538933)
