System Description: Spass Version 3.0

DOI10.1007/978-3-540-73595-3_38zbMATH Open1213.68577OpenAlexW1968191809MaRDI QIDQ3608799FDOQ3608799

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

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

Mathematics Subject Classification ID

Cited In (30)

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

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)