×

Found 4,393 Documents (Results 1–100)

Teaching linear algebra in a mechanized mathematical environment. (English) Zbl 07810727

Dubois, Catherine (ed.) et al., Intelligent computer mathematics. 16th international conference, CICM 2023, Cambridge, UK, September 5–8, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14101, 113-129 (2023).
MSC:  68Vxx
PDFBibTeX XMLCite
Full Text: DOI arXiv

Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. (English) Zbl 07768439

Lecture Notes in Computer Science 14132. Lecture Notes in Artificial Intelligence. Cham: Springer (ISBN 978-3-031-38498-1/pbk; 978-3-031-38499-8/ebook). xxv, 592 p., open access (2023).
PDFBibTeX XMLCite
Full Text: DOI

No, no, and no. (English) Zbl 07740528

Béziau, Jean-Yves (ed.) et al., Logic in question. Talks from the annual Sorbonne logic workshop (2011–2019), Paris, France, April 15–16, 2019. Cham: Birkhäuser. Stud. Univers. Log., 491-512 (2022).
PDFBibTeX XMLCite
Full Text: DOI

Direct elimination of additive-cuts in GL4ip: verified and extracted. (English) Zbl 1518.03015

Fernández-Duque, David (ed.) et al., Advances in modal logic. Vol. 14. Proceedings of the 14th conference (AiML 2022), Rennes, France, August 22–25, 2022. London: College Publications. 429-449 (2022).
MSC:  03F45 03B35 03F05
PDFBibTeX XMLCite

An essay on the foundations of geometry. With a new foreword by Michael Potter. Reprint of the 1897 edition. (English) Zbl 1520.51001

Routledge Classics. Milton Park, Abingdon: Routledge (ISBN 978-1-032-31264-4/hbk; 978-1-032-31226-2/pbk; 978-1-003-30887-4/ebook). xviii, 221 p. (2022).
PDFBibTeX XMLCite
Full Text: DOI

Mechanizing hypothesis formation. Principles and case studies. (English) Zbl 1502.68011

Boca Raton, FL: CRC Press/Science Publishers (ISBN 978-0-367-54980-0/hbk; 978-1-003-09144-8/ebook). xvi, 345 p. (2022).
PDFBibTeX XMLCite
Full Text: DOI

On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs. (English) Zbl 07570125

Hanus, Michael (ed.) et al., Functional and logic programming. 16th international symposium, FLOPS 2022, Kyoto, Japan, May 10–12, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13215, 262-281 (2022).
MSC:  03B35
PDFBibTeX XMLCite
Full Text: DOI

Formal topology and univalent foundations. (English) Zbl 1528.03251

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 255-266 (2022).
MSC:  03F65 03B35 03B38
PDFBibTeX XMLCite
Full Text: DOI

Who Finds the Short Proof? An Exploration of Variants of Boolos’ Curious Inference using Higher-order Automated Theorem Provers. arXiv:2208.06879

Preprint, arXiv:2208.06879 [math.LO] (2022).
BibTeX Cite
Full Text: DOI arXiv

Verified quadratic virtual substitution for real arithmetic. (English) Zbl 1521.68246

Huisman, Marieke (ed.) et al., Formal methods. 24th international symposium, FM 2021, virtual event, November 20–26, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13047, 200-217 (2021).
PDFBibTeX XMLCite
Full Text: DOI arXiv

A verified decision procedure for orders in Isabelle/HOL. (English) Zbl 1497.68549

Hou, Zhe (ed.) et al., Automated technology for verification and analysis. 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12971, 127-143 (2021).
MSC:  68V20 03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

The Lean 4 theorem prover and programming language. (English) Zbl 07437105

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 625-635 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

The Isabelle/Naproche natural language proof assistant. (English) Zbl 07437104

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 614-624 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Automatically building diagrams for olympiad geometry problems. (English) Zbl 07437101

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 577-588 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

A normative supervisor for reinforcement learning agents. (English) Zbl 07437100

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 565-576 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Reliable reconstruction of fine-grained proofs in a proof assistant. (English) Zbl 07437094

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 450-467 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Dual proof generation for quantified Boolean formulas with a BDD-based solver. (English) Zbl 07437093

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 433-449 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Superposition for full higher-order logic. (English) Zbl 1497.03030

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 396-412 (2021).
MSC:  03B35 03B16 68V15
PDFBibTeX XMLCite
Full Text: DOI

Superposition with first-class booleans and inprocessing clausification. (English) Zbl 07437090

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 378-395 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Generalized completeness for SOS resolution and its application to a new notion of relevance. (English) Zbl 07437087

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 327-343 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Computing optimal repairs of quantified ABoxes w.r.t. static \(\mathcal{EL}\) TBoxes. (English) Zbl 07437086

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 309-326 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Finding good proofs for description logic entailments using recursive quality measures. (English) Zbl 07437085

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 291-308 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Proof search and certificates for evidential transactions. (English) Zbl 07437082

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 234-251 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Unifying decidable entailments in separation logic with inductive definitions. (English) Zbl 07437079

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 183-199 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Politeness and stable infiniteness: stronger together. (English) Zbl 07437077

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 148-165 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Universal invariant checking of parametric systems with quantifier-free SMT reasoning. (English) Zbl 07437076

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 131-147 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints. (English) Zbl 07437075

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 113-130 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Isabelle’s metalogic: formalization and proof checker. (English) Zbl 07437074

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 93-110 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Efficient local reductions to basic modal logic. (English) Zbl 07437073

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 76-92 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Learning from Łukasiewicz and Meredith: investigations into proof structures. (English) Zbl 07437072

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 58-75 (2021).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Filter Results by …

Document Type

Database

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software