+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ Higher order proof reconstruction from paramodulation-based refutations:
+ the unit equality case
+ </span>
+ <a class="paper_download" href="PAPERS/hopr.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2007: The 6th
+ International Conference on Mathematical Knowledge Management.
+ </span>
+ <span class="paper_abstract">
+ In this paper we address the problem of reconstructing a
+ higher order, checkable proof object starting from a proof trace left by a
+ first order automatic proof searching procedure, in a restricted equational
+ framework. The automatic procedure is based on superposition rules for
+ the unit equality case. Proof transformation techniques aimed to improve
+ the readability of the final proof are discussed.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Spurious Disambiguation Error Detection
+ </span>
+ <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2007: The 6th
+ International Conference on Mathematical Knowledge Management.
+ </span>
+ <span class="paper_abstract">
+ The disambiguation approach to the input of formulae enables the user to
+ type correct formulae in a terse syntax close to the usual ambiguous
+ mathematical notation. When it comes to incorrect formulae we want to
+ present only errors related to the interpretation meant by the user, hiding
+ errors related to other interpretations (spurious errors). We propose a
+ heuristic to recognize spurious errors, which has been integrated with our
+ former efficient disambiguation algorithm.
+ </span>
+ </li>
+