scientific article; zbMATH DE number 976360
From MaRDI portal
Publication:4331764
Recommendations
Cited in
(38)- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- Completeness results for inequality provers
- Resolution methods for the decision problem
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- Model building with ordered resolution: Extracting models from saturated clause sets
- Deciding the E^+-class by an a posteriori, liftable order
- Formalization of the resolution calculus for first-order logic
- Working with ARMs: Complexity results on atomic representations of Herbrand models
- Hypothesis finding based on upward refinement of residue hypotheses.
- A superposition calculus for abductive reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Cut-elimination: syntax and semantics
- Blocking and other enhancements for bottom-up model generation methods
- Combining induction and saturation-based theorem proving
- Ceres in intuitionistic logic
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Towards a clausal analysis of cut-elimination
- Mechanising first-order temporal resolution
- Multimodal logic programming
- Controlling witnesses
- Formalization of the Resolution Calculus for First-Order Logic
- Combining instance generation and resolution
- scientific article; zbMATH DE number 516991 (Why is no real title available?)
- scientific article; zbMATH DE number 849903 (Why is no real title available?)
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- scientific article; zbMATH DE number 1418449 (Why is no real title available?)
- Adding Guarded Constructions to the Syllogistic
- Towards an algorithmic construction of cut-elimination procedures
- Analogy in automated deduction: a survey
- Cut-elimination and redundancy-elimination by resolution
- Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria
- Automated deduction
- Extracting Herbrand systems from refutation schemata
- Some techniques for reasoning automatically on co-inductive data structures
- The Resolution Calculus for First-Order Logic
- Group cancellation and resolution
- Representing and building models for decidable subclasses of equational clausal logic
- Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
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 Q4331764)
