SPASS & FLOTTER version 0.42

DOI10.1007/3-540-61511-3_75zbMath1412.68267OpenAlexW1543601803MaRDI QIDQ4647508

Christoph Weidenbach, Georg Rock, Bernd Gaede

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_75

Mathematics Subject Classification ID

Related Items

Reasoning without believing: on the mechanisation of presuppositions and partiality ⋮ Decidable Fragments of Many-Sorted Logic ⋮ Unifying splitting ⋮ Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators ⋮ FLOTTER ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ Integration of automated and interactive theorem proving in ILF ⋮ Soft typing for ordered resolution ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II

Uses Software

• OTTER
• SPASS

Cites Work

• Unnamed Item
• An erratum for some errata to ATP problems
• Attributive concept descriptions with complements
• Seventy-five problems for testing automatic theorem provers
• Schubert's steamroller problem: Formulations and solutions
• An optimality result for clause form translation
• Problem corner: The Lion and the Unicorn
• A note on assumptions about Skolem functions
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Substitution tree indexing