System Description: Spass Version 3.0

DOI10.1007/978-3-540-73595-3_38zbMath1213.68577OpenAlexW1968191809MaRDI QIDQ3608799

Rostislav Rusev, Dalibor Topić, Th. Hillenbrand, Renate A. Schmidt, Christoph Weidenbach

Publication date: 6 March 2009

Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_38

Mathematics Subject Classification ID

Related Items

Implementing Superposition in iProver (System Description), Automated Reasoning in the Wild, Simulation and Synthesis of Deduction Calculi, Reasoning without believing: on the mechanisation of presuppositions and partiality, A multi-clause dynamic deduction algorithm based on standard contradiction separation rule, Model evolution with equality -- revised and implemented, Theorem proving using clausal resolution: from past to present, A combined superposition and model evolution calculus, On Automating the Calculus of Relations, Modal Tools for Separation and Refinement, Using tableau to decide description logics with full role negation and identity, A resolution calculus for the branching-time temporal logic CTL, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, First-Order Resolution Methods for Modal Logics, Interpolation and Symbol Elimination in Vampire, Superposition and Model Evolution Combined, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, A Refined Resolution Calculus for CTL, Fair Derivations in Monodic Temporal Reasoning, On Transfinite Knuth-Bendix Orders, Blocking and other enhancements for bottom-up model generation methods, Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving, Unsorted Functional Translations, Labelled splitting, Automated verification of refinement laws, A new methodology for developing deduction methods, A FORMAL SYSTEM FOR EUCLID’SELEMENTS, Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL

Uses Software

• SPASS