Articles

1. Sequent Calculi for Choice Logics

   • Michael Bernreiter
   • Anela Lolic
   • Stefan Woltran

   OriginalPaper Open access 03 April 2024 Article: 8

   

2. Schematic Program Proofs with Abstract Execution

   • Dominic Steinhöfel
   • Reiner Hähnle

   OriginalPaper Open access 26 March 2024 Article: 7

   

3. SAT Meets Tableaux for Linear Temporal Logic Satisfiability

   • Luca Geatti
   • Nicola Gigante
   • Gabriele Venturato

   OriginalPaper Open access 15 March 2024 Article: 6

   

4. Should Decisions in QCDCL Follow Prefix Order?

   • Benjamin Böhm
   • Tomáš Peitl
   • Olaf Beyersdorff

   OriginalPaper Open access 09 February 2024 Article: 5

   

5. Non-termination in Term Rewriting and Logic Programming

   • Étienne Payet

   OriginalPaper 02 February 2024 Article: 4

   

6. A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry

   • David Braun
   • Nicolas Magaud
   • Pascal Schreck

   OriginalPaper 18 January 2024 Article: 3

   

7. A Formalization of the CHSH Inequality and Tsirelson’s Upper-bound in Isabelle/HOL

   • Mnacho Echenim
   • Mehdi Mhalla

   OriginalPaper 19 December 2023 Article: 2

   

8. Formally-Verified Round-Off Error Analysis of Runge–Kutta Methods

   • Florian Faissole

   OriginalPaper 06 December 2023 Article: 1

   

9. Formal Verification of Termination Criteria for First-Order Recursive Functions

   • Cesar A. Muñoz
   • Mauricio Ayala-Rincón
   • Thiago M. Ferreira Ramos

   OriginalPaper 29 November 2023 Article: 40

   

10. Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments

    • Sen Zheng
    • Renate A. Schmidt

    OriginalPaper Open access 23 November 2023 Article: 39

    

11. Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity

    • Xicheng Peng
    • Jingzhong Zhang
    • Sannyuya Liu

    OriginalPaper 20 November 2023 Article: 38

    

12. Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation

    • Andrzej Indrzejczak

    OriginalPaper Open access 16 November 2023 Article: 37

    

13. Finitary Type Theories With and Without Contexts

    • Philipp G. Haselwarter
    • Andrej Bauer

    OriginalPaper Open access 07 October 2023 Article: 36

    

14. Lower Bounds for QCDCL via Formula Gauge

    • Benjamin Böhm
    • Olaf Beyersdorff

    OriginalPaper Open access 27 September 2023 Article: 35

    

15. Combining Stable Infiniteness and (Strong) Politeness

    • Ying Sheng
    • Yoni Zohar
    • Cesare Tinelli

    Research 27 September 2023 Article: 34

    

16. Enabling Floating-Point Arithmetic in the Coq Proof Assistant

    • Érik Martin-Dorel
    • Guillaume Melquiond
    • Pierre Roux

    OriginalPaper 16 September 2023 Article: 33

    

17. Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences

    • Ying Sheng
    • Andres Nötzli
    • Cesare Tinelli

    OriginalPaper 15 September 2023 Article: 32

    

18. Preprocessing of Propagation Redundant Clauses

    • Joseph E. Reeves
    • Marijn J. H. Heule
    • Randal E. Bryant

    OriginalPaper Open access 14 September 2023 Article: 31

    

19. A Proof Procedure for Separation Logic with Inductive Definitions and Data

    • Mnacho Echenim
    • Nicolas Peltier

    OriginalPaper 09 September 2023 Article: 30

    

20. Mechanising Gödel–Löb Provability Logic in HOL Light

    • Marco Maggesi
    • Cosimo Perini Brogi

    OriginalPaper Open access 29 August 2023 Article: 29

    

21. Measure Construction by Extension in Dependent Type Theory with Application to Integration

    • Reynald Affeldt
    • Cyril Cohen

    OriginalPaper 18 August 2023 Article: 28

    

22. Cyclic Hypersequent System for Transitive Closure Logic

    • Anupam Das
    • Marianna Girlando

    OriginalPaper Open access 16 August 2023 Article: 27

    

23. A Resolution Proof System for Dependency Stochastic Boolean Satisfiability

    • Yun-Rong Luo
    • Che Cheng
    • Jie-Hong R. Jiang

    OriginalPaper 03 August 2023 Article: 26

    

24. Binary Codes that do not Preserve Primitivity

    • Štěpán Holub
    • Martin Raška
    • Štěpán Starosta

    OriginalPaper Open access 18 July 2023 Article: 25

    

25. POSIX Lexing with Derivatives of Regular Expressions

    • Christian Urban

    OriginalPaper Open access 08 July 2023 Article: 24

    

26. Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version

    • Andrei Popescu

    OriginalPaper Open access 05 July 2023 Article: 23

    

27. SCL(EQ): SCL for First-Order Logic with Equality

    • Hendrik Leidinger
    • Christoph Weidenbach

    OriginalPaper Open access 30 June 2023 Article: 22

    

28. A Formal Theory of Choreographic Programming

    • Luís Cruz-Filipe
    • Fabrizio Montesi
    • Marco Peressotti

    OriginalPaper Open access 27 May 2023 Article: 21

    

29. Combining Higher-Order Logic with Set Theory Formalizations

    • Cezary Kaliszyk
    • Karol Pąk

    OriginalPaper Open access 25 May 2023 Article: 20

    

30. Synthesising Programs with Non-trivial Constants

    • Alessandro Abate
    • Haniel Barbosa
    • Cesare Tinelli

    OriginalPaper Open access 13 May 2023 Article: 19

    

31. Engel’s Theorem in Mathlib

    • Oliver Nash

    OriginalPaper Open access 13 May 2023 Article: 18

    

32. An Automatically Verified Prototype of the Android Permissions System

    • Maximiliano Cristiá
    • Guido De Luca
    • Carlos Luna

    OriginalPaper 12 May 2023 Article: 17

    

33. Unifying Splitting

    • Gabriel Ebner
    • Jasmin Blanchette
    • Sophie Tourret

    OriginalPaper Open access 28 April 2023 Article: 16

    

34. An Automated Approach to the Collatz Conjecture

    • Emre Yolcu
    • Scott Aaronson
    • Marijn J. H. Heule

    OriginalPaper Open access 25 April 2023 Article: 15

35. First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification

    • Aart Middeldorp
    • Alexander Lochmann
    • Fabian Mitterwallner

    Research Open access 06 April 2023 Article: 14

    

36. Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

    • Dominik Kirst
    • Marc Hermes

    OriginalPaper Open access 12 March 2023 Article: 13

37. Computer-Aided Constructions of Commafree Codes

    • Aaron A. Windsor

    OriginalPaper 17 February 2023 Article: 12

38. Finding Normal Binary Floating-Point Factors Efficiently

    • Mak Andrlon

    OriginalPaper Open access 06 February 2023 Article: 11

    

39. Superposition for Higher-Order Logic

    • Alexander Bentkamp
    • Jasmin Blanchette
    • Petar Vukmirović

    OriginalPaper 21 January 2023 Article: 10

    

40. Correction: Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL

    • Richard Schmoetten
    • Jake E. Palmer
    • Jacques D. Fleuriot

    Correction Open access 13 January 2023 Article: 9

41. Efficient Extensional Binary Tries

    • Andrew W. Appel
    • Xavier Leroy

    OriginalPaper 12 January 2023 Article: 8

    

42. Optimal Deterministic Controller Synthesis from Steady-State Distributions

    • Alvaro Velasquez
    • Ismail Alkhouri
    • George Atia

    OriginalPaper 12 January 2023 Article: 7

    

43. Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover

    • Maria Paola Bonacina
    • Sarah Winkler

    OriginalPaper 11 January 2023 Article: 6

    

44. Measuring the Readability of Geometric Proofs: The Area Method Case

    • Pedro Quaresma
    • Pierluigi Graziani

    OriginalPaper Open access 10 January 2023 Article: 5

    

45. A Solver for Arrays with Concatenation

    • Qinshi Wang
    • Andrew W. Appel

    OriginalPaper 07 January 2023 Article: 4

    

46. Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

    • Guido Fiorino

    OriginalPaper 30 December 2022 Article: 3

    

47. Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL

    • Chelsea Edmonds
    • Angeliki Koutsoukou-Argyraki
    • Lawrence C. Paulson

    OriginalPaper Open access 19 December 2022 Article: 2

    

48. A Formalization and Proof Checker for Isabelle’s Metalogic

    • Simon Roßkopf
    • Tobias Nipkow

    OriginalPaper Open access 12 December 2022 Article: 1

49. Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL

    • Richard Schmoetten
    • Jake E. Palmer
    • Jacques D. Fleuriot

    OriginalPaper Open access 01 October 2022 Pages: 953 - 988

    

50. Correction to: Local is Best: Efficient Reductions to Modal Logic K

    • Fabio Papacchini
    • Cláudia Nalon
    • Clare Dixon

    Correction Open access 14 September 2022 Pages: 1099 - 1099