×

Found 24 Documents (Results 1–24)

100
MathJax

Public announcement logic in HOL. (English) Zbl 07437025

Martins, Manuel A. (ed.) et al., Dynamic logic. New trends and applications. Third international workshop, Dalí 2020, Prague, Czech Republic, October 9–10, 2020. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 12569, 222-238 (2020).
MSC:  03B42 68V15
PDF BibTeX XML Cite
Full Text: DOI arXiv

TacticToe: learning to reason with HOL4 tactics. (English) Zbl 1403.68224

Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 15-143 (2017).
MSC:  68T15 68T05
PDF BibTeX XML Cite
Full Text: DOI arXiv

Automatically proving equivalence by type-safe reflection. (English) Zbl 1367.68257

Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 40-55 (2017).
MSC:  68T15 68N30
PDF BibTeX XML Cite
Full Text: DOI Link

SEPIA: search for proofs using inferred automata. (English) Zbl 1465.68284

Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 246-255 (2015).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI arXiv

Mtac: a monad for typed tactic programming in Coq. (English) Zbl 1323.68236

Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP ’13, Boston, MA, USA, September 25–27, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2326-0). ACM SIGPLAN Notices 48, No. 9, 87-100 (2013).
MSC:  68N30 68T15
PDF BibTeX XML Cite
Full Text: DOI

How to make ad hoc proof automation less ad hoc. (English) Zbl 1323.68117

Proceedings of the 16th ACM SIGPLAN international conference on functional programming, ICFP ’11, Tokyo, Japan, September 19–21, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0865-6). ACM SIGPLAN Notices 46, No. 9, 163-175 (2011).
MSC:  68N18 68T15
PDF BibTeX XML Cite
Full Text: DOI Link

Automated certified proofs with CiME3. (English) Zbl 1236.68219

Schmid-Schauß, Manfred (ed.), 22nd international conference on rewriting techniques and applications (RTA 2011), Novi Sad, Serbia, May 30 – June 1, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-30-9). LIPIcs – Leibniz International Proceedings in Informatics 10, 21-30, electronic only (2011).
MSC:  68T15 68Q42
PDF BibTeX XML Cite
Full Text: DOI Link

Formalization of Wu’s simple method in Coq. (English) Zbl 1350.68234

Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 71-86 (2011).
MSC:  68T15
PDF BibTeX XML Cite
Full Text: DOI Link

Cut-simulation in impredicative logics. (English) Zbl 1159.03303

Furbach, Ulrich (ed.) et al., Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37187-8/pbk). Lecture Notes in Computer Science 4130. Lecture Notes in Artificial Intelligence, 220-234 (2006).
MSC:  03B35 03B15 03F05
PDF BibTeX XML Cite
Full Text: DOI

Filter Results by …

Document Type

Reviewing State

all top 5

Year of Publication

Classification

all top 3

Software