--- a/src/Doc/manual.bib Thu Nov 12 16:42:22 2020 +0100
+++ b/src/Doc/manual.bib Thu Nov 12 16:44:29 2020 +0100
@@ -587,6 +587,25 @@
publisher = CUP,
year = 1990}
+@inproceedings{de-moura-2008,
+ author = {Leonardo de Moura and
+ Nikolaj Bj{\o}rner},
+ editor = {C. R. Ramakrishnan and
+ Jakob Rehof},
+ title = {{Z3}: An Efficient {SMT} Solver},
+ booktitle = {Tools and Algorithms for the Construction and Analysis of Systems --- TACAS 2008},
+ series = {Lecture Notes in Computer Science},
+ volume = {4963},
+ pages = {337--340},
+ publisher = {Springer},
+ year = {2008},
+ url = {https://doi.org/10.1007/978-3-540-78800-3\_24},
+ doi = {10.1007/978-3-540-78800-3\_24},
+ timestamp = {Tue, 14 May 2019 10:00:53 +0200},
+ biburl = {https://dblp.org/rec/conf/tacas/MouraB08.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
@Book{devlin79,
author = {Keith J. Devlin},
title = {Fundamentals of Contemporary Set Theory},
@@ -1107,10 +1126,23 @@
title = {The Objective Caml system -- Documentation and user's manual},
note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}}
-@misc{agsyHOL,
- author = "Fredrik Lindblad",
- title = "{agsyHOL}",
- note = "\url{https://github.com/frelindb/agsyHOL}"}
+@inproceedings{agsyHOL,
+ author = {Fredrik Lindblad},
+ editor = {St{\'{e}}phane Demri and
+ Deepak Kapur and
+ Christoph Weidenbach},
+ title = {A Focused Sequent Calculus for Higher-Order Logic},
+ booktitle = {Automated Reasoning --- IJCAR 2014},
+ series = {Lecture Notes in Computer Science},
+ volume = {8562},
+ pages = {61--75},
+ publisher = {Springer},
+ year = {2014},
+ url = {https://doi.org/10.1007/978-3-319-08587-6\_5},
+ doi = {10.1007/978-3-319-08587-6\_5},
+ timestamp = {Tue, 14 May 2019 10:00:39 +0200},
+ biburl = {https://dblp.org/rec/conf/cade/Lindblad14.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}}
@incollection{lochbihler-2010,
title = "Coinductive",
@@ -1819,14 +1851,23 @@
number = 4
}
-@article{schulz-2002,
- author = "Stephan Schulz",
- title = "E---A Brainiac Theorem Prover",
- journal = "Journal of AI Communications",
- year = 2002,
- volume = 15,
- number ="2/3",
- pages = "111--126"}
+@inproceedings{schulz-2019,
+ author = {Stephan Schulz and
+ Simon Cruanes and
+ Petar Vukmirovi\'c},
+ editor = {Pascal Fontaine},
+ title = {Faster, Higher, Stronger: {E} 2.3},
+ booktitle = {Automated Deduction --- {CADE}-27},
+ series = {Lecture Notes in Computer Science},
+ volume = {11716},
+ pages = {495--507},
+ publisher = {Springer},
+ year = {2019},
+ url = {https://doi.org/10.1007/978-3-030-29436-6\_29},
+ doi = {10.1007/978-3-030-29436-6\_29},
+ timestamp = {Sat, 19 Oct 2019 20:28:03 +0200},
+ biburl = {https://dblp.org/rec/conf/cade/0001CV19.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}}
@inproceedings{slind-tfl,
author = {Konrad Slind},
@@ -2019,10 +2060,28 @@
note = {\url{http://x-symbol.sourceforge.net}}
}
-@misc{weidenbach-et-al-2009,
- author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski",
- title = "{SPASS} Version 3.5",
- note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}
+@inproceedings{weidenbach-et-al-2009,
+ author = {Christoph Weidenbach and
+ Dilyana Dimova and
+ Arnaud Fietzke and
+ Rohit Kumar and
+ Martin Suda and
+ Patrick Wischnewski},
+ editor = {Renate A. Schmidt},
+ title = {{SPASS} Version 3.5},
+ booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
+ Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
+ series = {Lecture Notes in Computer Science},
+ volume = {5663},
+ pages = {140--145},
+ publisher = {Springer},
+ year = {2009},
+ url = {https://doi.org/10.1007/978-3-642-02959-2\_10},
+ doi = {10.1007/978-3-642-02959-2\_10},
+ timestamp = {Tue, 14 May 2019 10:00:39 +0200},
+ biburl = {https://dblp.org/rec/conf/cade/WeidenbachDFKSW09.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
@manual{isabelle-system,
author = {Makarius Wenzel},
@@ -2255,13 +2314,6 @@
title = {On the Implementation of an Extensible Declarative Proof Language},
crossref = {tphols99}}
-%Z
-
-@misc{z3,
- key = "Z3",
- title = "Z3: An Efficient {SMT} Solver",
- note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"}
-
% CROSS REFERENCES