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)

• Improving automation for higher-order proof steps
• On the indestructibility aspects of identity crisis
• Superposition with lambdas
• scientific article; zbMATH DE number 7350767 (Why is no real title available?)
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Layered clause selection for theory reasoning (short paper)
• Superposition with lambdas
• Induction in saturation-based proof search

Describes a project that uses

Uses Software

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

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)