English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Conference Paper

Implementing the clausal normal form transformation with proof generation

MPS-Authors
/persons/resource/persons44298

de Nivelle,  Hans
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

de Nivelle, H. (2003). Implementing the clausal normal form transformation with proof generation. In Fourth Workshop on the Implementation of Logics (pp. 69-83). Liverpool, UK: University of Liverpool, University of Manchester.


Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2D33-5
Abstract
We explain how to implement the clausal normal form transformation with proof generation. We present a convenient data structure for sequent calculus proofs, which will be used for representing the generated proofs. The data structure allows easy proof checking and generation of proofs. In addition, it allows convenient implementation of proof normalization, which is necessary in order to keep the size of the generated proofs acceptable.