System Description: Spass Version 3.0
From MaRDI portal
Publication:3608799
Recommendations
Cited in
(31)- Blocking and other enhancements for bottom-up model generation methods
- Fair Derivations in Monodic Temporal Reasoning
- Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL
- Lash 1.0 (system description)
- A new methodology for developing deduction methods
- Simulation and synthesis of deduction calculi
- Harald Ganzinger's legacy: contributions to logics and programming
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Superposition and Model Evolution Combined
- A combined superposition and model evolution calculus
- Performance of clause selection heuristics for saturation-based theorem proving
- A Refined Resolution Calculus for CTL
- Using tableau to decide description logics with full role negation and identity
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- Automated verification of refinement laws
- scientific article; zbMATH DE number 2090305 (Why is no real title available?)
- Model evolution with equality -- revised and implemented
- Interpolation and symbol elimination in Vampire
- Implementing Superposition in iProver (System Description)
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- Modal tools for separation and refinement
- Automated reasoning in the wild
- On Automating the Calculus of Relations
- First-order resolution methods for modal logics
- Labelled splitting
- Theorem proving using clausal resolution: from past to present
- A resolution calculus for the branching-time temporal logic CTL
- Reasoning without believing: on the mechanisation of presuppositions and partiality
- System description: E-KRhyper 1.4. Extensions for unique names and description logic
- Unsorted functional translations
- On transfinite Knuth-Bendix orders
This page was built for publication: System Description: Spass Version 3.0
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608799)