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

Another footnote tweak

parent 47366fc1
No related branches found
No related tags found
1 merge request!1PxTP Extended Abstract
......@@ -126,8 +126,8 @@ reconstruction of proofs from the SMT solver CVC4~\cite{Barrett2011} in
Coq, where its proofs in the LFSC format~\cite{Stump2013} were
first translated into the veriT format before reconstruction.
%
Finally, the format will also be natively supported in the upcoming cvc5
solver\footnote{\url{https://cvc4.github.io/2021/04/02/cvc5-announcement.html}}.
Finally, the format will also be natively supported in the upcoming cvc5.
solver\footnote{\url{https://cvc4.github.io/2021/04/02/cvc5-announcement.html}}
On the one hand, Alethe uses a
natural-deduction style calculus driven mostly by resolution~\cite{besson-2011}.
......
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