Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
From MaRDI portal
Publication:5428267
DOI10.1007/978-3-540-73086-6_14zbMath1202.68370OpenAlexW1573383990MaRDI QIDQ5428267
Publication date: 28 November 2007
Published in: Towards Mechanized Mathematical Assistants (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-73086-6_14
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Hammer for Coq: automation for dependent type theory ⋮ An Interactive Driver for Goal-directed Proof Strategies ⋮ A Foundational View on Integration Problems
Uses Software
This page was built for publication: Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case