An abstraction-refinement framework for reasoning with large theories

DOI10.1007/978-3-319-94205-6_43MaRDI QIDQ1799131zbMATH OpenOpenAlexFDO

Authors Julio Cesar Lopez Hernandez, Konstantin Korovin

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

abstraction refinementautomated reasoninglarge theories

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4164177
• Sine qua non for large theory reasoning
• scientific article; zbMATH DE number 1341620
• scientific article; zbMATH DE number 139760
• Lemmatization for stronger reasoning in large theories

Cited in

(11)

• GKC: a reasoning system for large knowledge bases
• Structure formation in large theories
• Large theory reasoning with SUMO at CASC
• Implementing Superposition in iProver (System Description)
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• Sine qua non for large theory reasoning
• Scalable reasoning by abstraction beyond DL-Lite
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Machine learning for quantifier selection in cvc5
• The QSMA algorithm for quantifiers in SMT
• Learning guided automated reasoning: a brief survey

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1799131)