System Description: Spass Version 3.0

DOI10.1007/978-3-540-73595-3_38MaRDI QIDQ3608799zbMATH OpenOpenAlexFDO

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

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

Recommendations

• System description: SPASS-FD
• scientific article; zbMATH DE number 2090305
• System description: GAPT 2.0
• System description: E 1.8
• System description: E.T. 0.1
• Automated Reasoning
• scientific article; zbMATH DE number 2090306
• scientific article; zbMATH DE number 1614711

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

Describes a project that uses

Uses Software

• SPASS

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)