Extensional Crisis and Proving Identity

DOI10.1007/978-3-319-11936-6_14zbMath1448.68459OpenAlexW182525246MaRDI QIDQ3457789

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

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)

Related Items (7)

Improving automation for higher-order proof steps ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ Induction in saturation-based proof search ⋮ Layered clause selection for theory reasoning (short paper)

Uses Software

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

This page was built for publication: Extensional Crisis and Proving Identity