×

Found 277 Documents (Results 1–100)

Towards substructural property-based testing. (English) Zbl 1521.68035

De Angelis, Emanuele (ed.) et al., Logic-based program synthesis and transformation. 31st international symposium, LOPSTR 2021, Tallinn, Estonia, September 7–8, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13290, 92-112 (2022).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Generalized arrays for Stainless frames. (English) Zbl 1498.68172

Finkbeiner, Bernd (ed.) et al., Verification, model checking, and abstract interpretation. 23rd international conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13182, 332-354 (2022).
PDFBibTeX XMLCite
Full Text: DOI

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

Formalizing axiomatic systems for propositional logic in Isabelle/HOL. (English) Zbl 1485.68292

Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 32-46 (2021).
MSC:  68V20 03B05 03B20
PDFBibTeX XMLCite
Full Text: DOI Link

Experiments in causality and STIT. (English) Zbl 1484.68314

Liao, Beishui (ed.) et al., Logics for new-generation AI 2021. First international workshop, LNGAI 2021, June, 18–20 2021, Hangzhou, China. London: College Publications. 33-45 (2021).
MSC:  68V15 03B42 68T27
PDFBibTeX XMLCite

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

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

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

Deductive stability proofs for ordinary differential equations. (English) Zbl 1474.68195

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 181-199 (2021).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Computer-supported exploration of a categorical axiomatization of modeloids. (English) Zbl 1509.68328

Fahrenberg, Uli (ed.) et al., Relational and algebraic methods in computer science. 18th international conference, RAMiCS 2020, Palaiseau, France, October 26–29, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12062, 302-317 (2020).
PDFBibTeX XMLCite
Full Text: DOI arXiv

An efficient normalisation procedure for linear temporal logic and very weak alternating automata. (English) Zbl 07299516

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 831-844 (2020).
MSC:  68-XX 03B44
PDFBibTeX XMLCite
Full Text: DOI arXiv

A mechanized proof of Higman’s lemma by open induction. (English) Zbl 1446.68188

Schuster, Peter M. (ed.) et al., Well-quasi orders in computation, logic, language and reasoning. A unifying concept of proof theory, automata theory, formal languages and descriptive set theory. Based on the minisymposium on well-quasi orders: from theory to applications within the Jahrestagung der Deutschen Mathematiker-Vereinigung (DMV), Hamburg, Germany, September 21–25, 2015 and the Dagstuhl seminar 16031 on well quasi-orders in computer science, Schloss Dagstuhl, Germany, January 17–22, 2016. Cham: Springer. Trends Log. Stud. Log. Libr. 53, 339-350 (2020).
MSC:  68V20 03B35 03E05
PDFBibTeX XMLCite
Full Text: DOI

Formalising mathematics in simple type theory. (English) Zbl 1528.03098

Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 437-453 (2019).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Herbrand constructivization for automated intuitionistic theorem proving. (English) Zbl 1435.68364

Cerrito, Serenella (ed.) et al., Automated reasoning with analytic tableaux and related methods. 28th international conference, TABLEAUX 2019, London, UK, September 3–5, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11714, 355-373 (2019).
MSC:  68V15 03B20 03B35
PDFBibTeX XMLCite
Full Text: DOI

Certified equational reasoning via ordered completion. (English) Zbl 07178995

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 508-525 (2019).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

A formally verified abstract account of Gödel’s incompleteness theorems. (English) Zbl 07178991

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 442-461 (2019).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI Link

Towards bit-width-independent proofs in SMT solvers. (English) Zbl 07178987

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 366-384 (2019).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\). (English) Zbl 07178977

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 197-215 (2019).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

GRUNGE: a grand unified ATP challenge. (English) Zbl 07178973

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 123-141 (2019).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

\(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic. (English) Zbl 07178971

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 94-110 (2019).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI

Extending SMT solvers to higher-order logic. (English) Zbl 07178968

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 35-54 (2019).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI HAL

Formalized proof systems for propositional logic. (English) Zbl 1528.03097

Abel, Andreas (ed.) et al., 23rd international conference on types for proofs and programs, TYPES 2017, May 24 – June 1, 2017, Budapest, Hungary. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 104, Article 5, 16 p. (2018).
MSC:  03B35
PDFBibTeX XMLCite
Full Text: DOI

The MET: the art of flexible reasoning with modalities. (English) Zbl 1518.68416

Benzmüller, Christoph (ed.) et al., Rules and reasoning. Second international joint conference, RuleML+RR 2018, Luxembourg, Luxembourg, September 18–21, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11092, 274-284 (2018).
MSC:  68V15 03B45
PDFBibTeX XMLCite
Full Text: DOI

Model-theoretic conservative extension for definitional theories. (English) Zbl 1434.03028

Alves, Sandra (ed.) et al., Selected papers of the 12th workshop on logical and semantic frameworks, with applications (LSFA 2017), Brasilia, Brazil, September 23–24, 2017. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 338, 133-145 (2018).
PDFBibTeX XMLCite
Full Text: DOI

Hoare logics for time bounds. A study in meta theory. (English) Zbl 1423.68098

Beyer, Dirk (ed.) et al., Tools and algorithms for the construction and analysis of systems. 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 10805, 155-171 (2018).
MSC:  68N30 03B70 68Q60 68T15 68W40
PDFBibTeX XMLCite
Full Text: DOI

A dyadic deontic logic in HOL. (English) Zbl 1418.03069

Broersen, Jan (ed.) et al., Deontic logic and normative systems. 14th international conference, DEON 2018, Utrecht, Netherlands, July 3–6, 2018. Proceedings. London: College Publications. 33-49 (2018).
MSC:  03B45 03B15 03B35
PDFBibTeX XMLCite

Verifying hybrid systems with modal Kleene algebra. (English) Zbl 1518.68209

Desharnais, Jules (ed.) et al., Relational and algebraic methods in computer science. 17th international conference, RAMiCS 2018, Groningen, The Netherlands, October 29 – November 1, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11194, 225-243 (2018).
MSC:  68Q60 03B70 68V20
PDFBibTeX XMLCite
Full Text: DOI

Formalizing Bachmair and Ganzinger’s ordered resolution prover. (English) Zbl 1468.68306

Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 89-107 (2018).
MSC:  68V15 03B35 68V20
PDFBibTeX XMLCite
Full Text: DOI Link

Superposition for \(\lambda\)-free higher-order logic. (English) Zbl 1511.68302

Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 28-46 (2018).
MSC:  68V15 03B16 03B35
PDFBibTeX XMLCite
Full Text: DOI

Program verification in the presence of cached address translation. (English) Zbl 1468.68069

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, 542-559 (2018).
PDFBibTeX XMLCite
Full Text: DOI

Verifying the LTL to Büchi automata translation via very weak alternating automata. (English) Zbl 1511.68335

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, 306-323 (2018).
PDFBibTeX XMLCite
Full Text: DOI

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).
PDFBibTeX XMLCite
Full Text: DOI HAL

Backwards and forwards with separation logic. (English) Zbl 1511.68067

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, 68-87 (2018).
MSC:  68N30 03B70 68V15
PDFBibTeX XMLCite
Full Text: DOI

Software tool support for modular reasoning in modal logics of actions. (English) Zbl 1511.68301

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, 48-67 (2018).
PDFBibTeX XMLCite
Full Text: DOI Link

A deontic logic reasoning infrastructure. (English) Zbl 1509.68327

Manea, Florin (ed.) et al., Sailing routes in the world of computation. 14th conference on computability in Europe, CiE 2018, Kiel, Germany, July 30 – August 3, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10936, 60-69 (2018).
PDFBibTeX XMLCite
Full Text: DOI Link

Foundational nonuniform (co)datatypes for higher-order logic. (English) Zbl 1457.68173

Proceedings of the 2017 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017, Reykjavík University, Reykjavík, Iceland, June 20–23, 2017. Piscataway, NJ: IEEE Press. Article No. 11, 12 p. (2017).
MSC:  68Q65 03B16
PDFBibTeX XMLCite
Full Text: Link

Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. (English) Zbl 1434.03025

Miller, Dale (ed.), 2nd international conference on formal structures for computation and deduction. FSCD 2017, Oxford, UK, September 3–9, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 84, Article 11, 18 p. (2017).
MSC:  03B35 03B25 03F15
PDFBibTeX XMLCite
Full Text: DOI

Theorem provers for every normal modal logic. (English) Zbl 1403.68225

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, 14-30 (2017).
MSC:  68T15 03B35 03B45
PDFBibTeX XMLCite
Full Text: DOI

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software