Efficient encodings of first-order Horn formulas in equational logic
From MaRDI portal
Publication:1799100
DOI10.1007/978-3-319-94205-6_26OpenAlexW2811206835MaRDI QIDQ1799100
Nicholas Smallbone, Koen Claessen
Publication date: 18 October 2018
Full work available at URL: https://research.chalmers.se/en/publication/504180
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (6)
The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ Twee: an equational theorem prover ⋮ Ground joinability and connectedness in the superposition calculus
Uses Software
This page was built for publication: Efficient encodings of first-order Horn formulas in equational logic
