Twee: an equational theorem prover

DOI10.1007/978-3-030-79876-5_35OpenAlexW3182937571MaRDI QIDQ2055894

Nicholas Smallbone

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_35

zbMATH Keywords

completionautomated theorem provingunit equality

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

AC simplifications and closure redundancies in the superposition calculus ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Twee: an equational theorem prover ⋮ Ground joinability and connectedness in the superposition calculus ⋮ Guiding an automated theorem prover with neural rewriting

Uses Software

• LCF
• MadMax
• Twee
• Jukebox

Cites Work

• Unnamed Item
• Unnamed Item
• Things to know when implementing KBO
• Critical pair criteria for completion
• On using ground joinable equations in equational theorem proving
• Efficient encodings of first-order Horn formulas in equational logic
• MædMax: a maximal ordered completion tool
• Edinburgh LCF. A mechanized logic of computation
• Twee: an equational theorem prover
• Faster, higher, stronger: E 2.3
• Recording and analysing knowledge-based distributed deduction processes
• Sort It Out with Monotonicity
• Deciding the confluence of ordered term rewrite systems

This page was built for publication: Twee: an equational theorem prover