An abstraction-refinement framework for reasoning with large theories

DOI10.1007/978-3-319-94205-6_43OpenAlexW2809879880MaRDI QIDQ1799131

Konstantin Korovin, Julio Cesar Lopez Hernandez

Publication date: 18 October 2018

Full work available at URL: http://www.cs.man.ac.uk/~korovink/my_pub/abstr_ref_ijcar_2018.pdf

zbMATH Keywords

automated reasoningabstraction refinementlarge theories

Mathematics Subject Classification ID

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

Related Items (4)

Implementing Superposition in iProver (System Description) ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ GKC: a reasoning system for large knowledge bases

Uses Software

• LEO-II
• VAMPIRE
• TPTP
• HOL Light
• Sledgehammer
• CakeML
• iProver
• MaLARea
• HOLyHammer
• SRASS

This page was built for publication: An abstraction-refinement framework for reasoning with large theories