System Description: SPASS-FD

DOI10.1007/978-3-642-22438-6_25zbMath1341.68190OpenAlexW1752605800MaRDI QIDQ5200034

Matthias Horbach

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_25

Mathematics Subject Classification ID

Related Items (1)

Predicate Completion for non-Horn Clause Sets

Uses Software

• SPASS
• TPTP
• Spass-FD

Cites Work

• Unnamed Item
• Unnamed Item
• Equational problems and disunification
• Induction = I-axiomatization + first-order consistency.
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Superposition for fixed domains
• Disunification for Ultimately Periodic Interpretations
• Deciding the Inductive Validity of ∀ ∃ * Queries
• Decidability Results for Saturation-Based Model Building
• Predicate Completion for non-Horn Clause Sets
• Automated Deduction – CADE-20
• Automated Deduction – CADE-19

This page was built for publication: System Description: SPASS-FD