Doczkal, Christian; Pous, Damien Graph theory in Coq: minors, treewidth, and isomorphisms. (English) Zbl 1468.68320 J. Autom. Reasoning 64, No. 5, 795-825 (2020). MSC: 68V20 03B35 05C05 05C40 05C60 05C83 PDFBibTeX XMLCite \textit{C. Doczkal} and \textit{D. Pous}, J. Autom. Reasoning 64, No. 5, 795--825 (2020; Zbl 1468.68320) Full Text: DOI HAL
Doczkal, Christian; Combette, Guillaume; Pous, Damien A formal proof of the minor-exclusion property for treewidth-two graphs. (English) Zbl 1468.68319 Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 178-195 (2018). MSC: 68V20 03B35 05C05 05C60 05C83 68V15 PDFBibTeX XMLCite \textit{C. Doczkal} et al., Lect. Notes Comput. Sci. 10895, 178--195 (2018; Zbl 1468.68319) Full Text: DOI HAL
Palmgren, Erik Constructions of categories of setoids from proof-irrelevant families. (English) Zbl 1390.03013 Arch. Math. Logic 56, No. 1-2, 51-66 (2017). Reviewer: Marco Benini (Buccinasco) MSC: 03B15 18B05 18B15 PDFBibTeX XMLCite \textit{E. Palmgren}, Arch. Math. Logic 56, No. 1--2, 51--66 (2017; Zbl 1390.03013) Full Text: DOI
Steen, Alexander; Benzmüller, Christoph Sweet SIXTEEN: automation via embedding into classical higher-order logic. (English) Zbl 1373.03030 Log. Log. Philos. 25, No. 4, 535-554 (2016). Reviewer: Matteo Bianchi (Milano) MSC: 03B50 03B15 PDFBibTeX XMLCite \textit{A. Steen} and \textit{C. Benzmüller}, Log. Log. Philos. 25, No. 4, 535--554 (2016; Zbl 1373.03030) Full Text: DOI
Zeyda, Frank; Cavalcanti, Ana Mechanical reasoning about families of UTP theories. (English) Zbl 1243.68270 Sci. Comput. Program. 77, No. 4, 444-479 (2012). MSC: 68T15 68N15 68Q60 PDFBibTeX XMLCite \textit{F. Zeyda} and \textit{A. Cavalcanti}, Sci. Comput. Program. 77, No. 4, 444--479 (2012; Zbl 1243.68270) Full Text: DOI
Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine Verifying B proof rules using deep embedding and automated theorem proving. (English) Zbl 1350.68236 Barthe, Gilles (ed.) et al., Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14–18, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24689-0/pbk). Lecture Notes in Computer Science 7041, 253-268 (2011). MSC: 68T15 68N30 68Q60 PDFBibTeX XMLCite \textit{M. Jacquel} et al., Lect. Notes Comput. Sci. 7041, 253--268 (2011; Zbl 1350.68236) Full Text: DOI
Ripon, Shamim H.; Butler, Michael J. PVS embedding of cCSP semantic models and their relationship. (English) Zbl 1335.68129 Miller, Alice (ed.) et al., Proceedings of the 8th international workshop on automated verification of critical systems (AVoCS 2008), Glasgow, UK, September 30 – October 1, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 250, No. 2, 103-118 (2009). MSC: 68Q55 68Q60 68Q85 PDFBibTeX XMLCite \textit{S. H. Ripon} and \textit{M. J. Butler}, Electron. Notes Theor. Comput. Sci. 250, No. 2, 103--118 (2009; Zbl 1335.68129) Full Text: DOI
Jaeger, Éric; Dubois, Catherine Why would you trust \(B\)? (English) Zbl 1137.68355 Dershowitz, Nachum (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 14th international conference, LPAR 2007, Yerevan, Armenia, October 15–19, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75558-6/pbk). Lecture Notes in Computer Science 4790. Lecture Notes in Artificial Intelligence, 288-302 (2007). MSC: 68N30 03B70 68Q60 68T15 PDFBibTeX XMLCite \textit{É. Jaeger} and \textit{C. Dubois}, Lect. Notes Comput. Sci. 4790, 288--302 (2007; Zbl 1137.68355) Full Text: DOI