×

Found 1,742 Documents (Results 1–100)

100
MathJax

Tests and proofs. 16th international conference, TAP 2022, held as part of STAF 2022, Nantes, France, July 5, 2022. Proceedings. (English) Zbl 07554836

Lecture Notes in Computer Science 13361. Cham: Springer (ISBN 978-3-031-09826-0/pbk; 978-3-031-09827-7/ebook). viii, 125 p. (2022).
PDF BibTeX XML Cite
Full Text: DOI

Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26–27, 2022. (English) Zbl 07545246

Electronic Proceedings in Theoretical Computer Science (EPTCS) 359. Waterloo: Open Publishing Association (OPA). 216 p., electronic only, open access (2022).
PDF BibTeX XML Cite
Full Text: DOI Link

Proceedings of the 13th international conference on automated deduction in geometry, Hagenberg, Austria/virtual, September 15–17, 2021. (English) Zbl 07545242

Electronic Proceedings in Theoretical Computer Science (EPTCS) 352. Waterloo: Open Publishing Association (OPA). 172 p., electronic only, open access (2021).
PDF BibTeX XML Cite
Full Text: DOI Link

Proceedings of the seventh workshop on proof eXchange for theorem proving, Pittsburg, USA, July 11, 2021. (English) Zbl 07544348

Electronic Proceedings in Theoretical Computer Science (EPTCS) 336. Waterloo: Open Publishing Association (OPA). 54 p., electronic only, open access (2021).
MSC:  68-06 68V15 00B25
PDF BibTeX XML Cite
Full Text: DOI Link

The Došen square under construction: a tale of four modalities. (English) Zbl 07532531

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 446-465 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Game semantics for constructive modal logic. (English) Zbl 07532530

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 428-445 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Nested sequents for intuitionistic modal logics via structural refinement. (English) Zbl 07532529

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 409-427 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Terminating calculi and countermodels for constructive modal logics. (English) Zbl 07532528

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 391-408 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

A focus system for the alternation-free \(\mu \)-calculus. (English) Zbl 07532527

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 371-388 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Cyclic hypersequent calculi for some modal logics with the master modality. (English) Zbl 07532526

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 354-370 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Uniform interpolation from cyclic proofs: the case of modal mu-calculus. (English) Zbl 07532525

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 335-353 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs. (English) Zbl 07532524

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 317-334 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq. (English) Zbl 07532523

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 299-313 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

A formally verified cut-elimination procedure for linear nested sequents for tense logic. (English) Zbl 07532522

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 281-298 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Learning theorem proving components. (English) Zbl 07532521

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 266-278 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Eliminating models during model elimination. (English) Zbl 07532520

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 250-265 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

The nanoCoP 2.0 connection provers for classical, intuitionistic and modal logics. (English) Zbl 07532519

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 236-249 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

The role of entropy in guiding a connection prover. (English) Zbl 07532518

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 218-235 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

AC simplifications and closure redundancies in the superposition calculus. (English) Zbl 07532517

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 200-217 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

lazyCoP: lazy paramodulation meets neurally guided search. (English) Zbl 07532516

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 187-199 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Towards finding longer proofs. (English) Zbl 07532515

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 167-186 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

From input/output logics to conditional logics via sequents – with provers. (English) Zbl 07532514

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 147-164 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Proof search on bilateralist judgments over non-deterministic semantics. (English) Zbl 07532513

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 129-146 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Basing sequent systems on exclusive-or. (English) Zbl 07532512

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 112-128 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT. (English) Zbl 07532510

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 74-91 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Tableaux for free logics with descriptions. (English) Zbl 07532509

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 56-73 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Constraint tableaux for two-dimensional fuzzy logics. (English) Zbl 07532507

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 20-37 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Tableaux and restricted quantification for systems related to weak Kleene logic. (English) Zbl 07532506

Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 3-19 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Automated generation of exam sheets for automated deduction. (English) Zbl 1485.68283

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, 185-196 (2021).
MSC:  68V15 97D60
PDF BibTeX XML Cite
Full Text: DOI

Inductive benchmarks for automated reasoning. (English) Zbl 1485.68281

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, 124-129 (2021).
MSC:  68V15
PDF BibTeX XML Cite
Full Text: DOI

Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. (English) Zbl 1485.68282

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, 107-123 (2021).
MSC:  68V15 68T05 68T20
PDF BibTeX XML Cite
Full Text: DOI

Improving stateful premise selection with transformers. (English) Zbl 1485.68286

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, 84-89 (2021).
MSC:  68V15 68T05
PDF BibTeX XML Cite
Full Text: DOI

Online machine learning techniques for Coq: a comparison. (English) Zbl 1485.68288

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, 67-83 (2021).
MSC:  68V15 68T05 68W27
PDF BibTeX XML Cite
Full Text: DOI

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
PDF BibTeX XML Cite

A flexible approach to argumentation framework analysis using theorem proving. (English) Zbl 1484.68228

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. 18-32 (2021).
MSC:  68T27 68V15
PDF BibTeX XML Cite

Harpoon: mechanizing metatheory interactively. (English) Zbl 07437106

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, 636-648 (2021).
MSC:  03B35 68V15
PDF BibTeX XML Cite
Full Text: DOI

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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
Full Text: DOI

An automated approach to the Collatz conjecture. (English) Zbl 07437095

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, 468-484 (2021).
MSC:  03B35 68V15
PDF BibTeX XML Cite
Full Text: DOI arXiv

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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
Full Text: DOI

Making higher-order superposition work. (English) Zbl 07437092

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, 415-432 (2021).
MSC:  03B35 68V15
PDF BibTeX XML Cite
Full Text: DOI

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

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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
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
PDF BibTeX XML Cite
Full Text: DOI

Filter Results by …

Document Type

Reviewing State

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Classification

all top 3

Software