Extensional crisis and proving identity

DOI10.1007/978-3-319-11936-6_14zbMATH Open1448.68459OpenAlexW182525246MaRDI QIDQ3457789FDOQ3457789

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

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

zbMATH Keywords

extensionalityextensionality resolutionVampire

Mathematics Subject Classification ID

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

Cited In (8)

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

Uses Software

• VAMPIRE
• SMT-LIB
• TPTP
• SPASS+T
• z3
• 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)