Skip to content
Snippets Groups Projects
Commit 4aa507c7 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Merge branch 'master' of gitlab.uliege.be:verit/proof-format

parents 64b7e48b dd081ad3
No related branches found
No related tags found
No related merge requests found
Pipeline #3369 failed
......@@ -269,3 +269,38 @@
year = {2021},
series = lncs,
}
@article{de-nivelle-2005,
author = {Hans de Nivelle},
title = {Translation of resolution proofs into short first-order proofs without
choice axioms},
journal = {Inf. Comput.},
volume = {199},
number = {1-2},
pages = {24--54},
year = {2005}
}
@inproceedings{paulson-susanto-2007,
author = {Lawrence C. Paulson and Kong Woei Susanto},
booktitle = {TPHOLs 2007},
editor = {Klaus Schneider and Jens Brandt},
title = {Source-Level Proof Reconstruction for Interactive Theorem Proving},
pages = {232--245},
series = lncs,
publisher = {Springer},
volume = {4732},
year = {2007}
}
@inproceedings{boehme-weber-2010,
author = {Sascha B{\"o}hme and Tjark Weber},
title = {Fast {LCF}-Style Proof Reconstruction for {Z3}},
publisher = "Springer",
series = lncs,
year = 2010,
editor = "Matt Kaufmann and Lawrence Paulson",
booktitle = "ITP 2010",
volume = 6172,
pages = "179--194"
}
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment