Efficient encodings of first-order Horn formulas in equational logic

DOI10.1007/978-3-319-94205-6_26MaRDI QIDQ1799100

Koen Claessen, Nicholas Smallbone

Publication date: 18 October 2018

Full work available at URL: https://research.chalmers.se/en/publication/504180

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

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

Uses Software

• SPASS
• TPTP
• E Theorem Prover
• Waldmeister
• Twee