Pages that link to "Item:Q3608799"
From MaRDI portal
The following pages link to System Description: Spass Version 3.0 (Q3608799):
Displaying 28 items.
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- A combined superposition and model evolution calculus (Q438531) (← links)
- Labelled splitting (Q1037396) (← links)
- Automated verification of refinement laws (Q1037397) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL (Q2104508) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Theorem proving using clausal resolution: from past to present (Q2695485) (← links)
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (Q2817933) (← links)
- Unsorted Functional Translations (Q2825403) (← links)
- Simulation and Synthesis of Deduction Calculi (Q3185770) (← links)
- Automated Reasoning in the Wild (Q3454081) (← links)
- On Automating the Calculus of Relations (Q3541686) (← links)
- Reasoning without believing: on the mechanisation of presuppositions and partiality (Q4583173) (← links)
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
- First-Order Resolution Methods for Modal Logics (Q4916086) (← links)
- Implementing Superposition in iProver (System Description) (Q5049017) (← links)
- Superposition and Model Evolution Combined (Q5191094) (← links)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic (Q5191100) (← links)
- A Refined Resolution Calculus for CTL (Q5191106) (← links)
- Fair Derivations in Monodic Temporal Reasoning (Q5191107) (← links)
- On Transfinite Knuth-Bendix Orders (Q5200038) (← links)
- Modal Tools for Separation and Refinement (Q5403464) (← links)
- Using tableau to decide description logics with full role negation and identity (Q5410334) (← links)
- A resolution calculus for the branching-time temporal logic CTL (Q5410337) (← links)
- Interpolation and Symbol Elimination in Vampire (Q5747760) (← links)
- A FORMAL SYSTEM FOR EUCLID’S<i>ELEMENTS</i> (Q5850985) (← links)
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule (Q6086313) (← links)
