KoMeT

DOI10.1007/3-540-58156-1_60zbMath1433.68535OpenAlexW4254134740MaRDI QIDQ5210812

Thomas Rath, Stefan Brüning, Uwe Egly, Wolfgang Bibel

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_60

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (8)

ILF-SETHEO ⋮ IeanCOP: lean connection-based theorem proving ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ T-string unification: Unifying prefixes in non-classical proof methods ⋮ Converting non-classical matrix proofs into sequent-style systems ⋮ Prolog technology for default reasoning: proof theory and compilation techniques ⋮ Integration of automated and interactive theorem proving in ILF ⋮ A uniform procedure for converting matrix proofs into sequent-style systems

Uses Software

• SETHEO

Cites Work

• A structure-preserving clause form translation
• Schubert's steamroller problem: Formulations and solutions
• SETHEO: A high-performance theorem prover
• Proving Theorems with the Modification Method
• Theorem proving using equational matings and rigid E -unification
• A Machine-Oriented Logic Based on the Resolution Principle
• An automatic proof of Gödel's incompleteness theorem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: KoMeT