Extensional crisis and proving identity

DOI10.1007/978-3-319-11936-6_14MaRDI QIDQ3457789zbMATH OpenOpenAlexFDO

Authors Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov

Publication date 17 December 2015

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-11936-6_14

zbMATH Keywords

extensionalityextensionality resolutionVampire

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2213626
• Automated Deduction – CADE-20
• Extensional set equality in the calculus of constructions
• Automata, Languages and Programming
• scientific article; zbMATH DE number 4164184

Cited in

(8)

• Layered clause selection for theory reasoning (short paper)
• Induction in saturation-based proof search
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Superposition for lambda-free higher-order logic
• Superposition with lambdas
• Superposition with lambdas
• Improving automation for higher-order proof steps
• On the indestructibility aspects of identity crisis

Describes a project that uses

Uses Software

• VAMPIRE
• TPTP
• z3
• SMT-LIB
• SPASS+T
• CVC4
• iProver

This page was built for publication: Extensional crisis and proving identity

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