Skip to main content
main-content

Journal of Automated Reasoning OnlineFirst articles

Open Access 01-10-2022

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

Special relativity is a cornerstone of modern physical theory. While a standard coordinate model is well known and widely taught today, multiple axiomatic systems for SR have been constructed over the past century. This paper reports on the …

Authors:
Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot

Open Access 14-09-2022 | Correction

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

Unfortunately in the original publication of the article, several typo errors found in the mathematical symbols, spacing and layout of Tables 1 and 3 which are incorrectly processed throughout the article. The original article has been corrected.

Authors:
Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon

12-09-2022

Pardinus: A Temporal Relational Model Finder

This article presents $$\mathsf {Pardinus}$$ Pardinus , an extension of the popular $$\mathsf {Kodkod}$$ Kodkod relational model finder with linear temporal logic (including past operators), to simplify the analysis of dynamic systems. $$\mathsf …

Authors:
Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha

Open Access 08-09-2022

A Formalization of Dedekind Domains and Class Groups of Global Fields

Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number-theoretic finiteness results for class …

Authors:
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio

12-08-2022

Faster Linear Unification Algorithm

The Robinson unification algorithm has exponential worst case behavior. This triggered the development of (semi-)linear versions around 1976 by Martelli and Montanari as well as by Paterson and Wegman (J Comput Syst Sci 16(2):158–167, 1978 …

Author:
Dennis de Champeaux

11-08-2022

From Specification to Testing: Semantics Engineering for Lua 5.2

We provide a formal semantics for a large subset of the Lua programming language, in its version 5.2. The semantics is a major part of an ongoing effort to construct reliable tools to analyze Lua code. In this work, we present the details of …

Authors:
Mallku Soldevila, Beta Ziliani, Bruno Silvestre

Open Access 06-08-2022 | Correction

Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic

Under the section heading “3 A Connection Between the JNF Library and the HA Library with the mod_type Restriction”, at certain places the type variables 'n and 'm were published erroneously without the prime in front, so that they appeared as …

Authors:
Jose Divasón, René Thiemann

Open Access 27-07-2022

A Formalization of SQL with Nulls

SQL is the world’s most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification.

Authors:
Wilmer Ricciotti, James Cheney

25-07-2022

Tuple Interpretations for Termination of Term Rewriting

Interpretation methods constitute a foundation of the termination analysis of term rewriting. From time to time, remarkable instances of interpretation methods appeared, such as polynomial interpretations, matrix interpretations, arctic …

Author:
Akihisa Yamada

18-07-2022

Six Decades of Automated Reasoning: Papers in Memory of Larry Wos

Foreword
Author:
Maria Paola Bonacina

06-07-2022

Fast Left Kan Extensions Using the Chase

We show how computation of left Kan extensions can be reduced to computation of free models of cartesian (finite-limit) theories. We discuss how the standard and parallel chase compute weakly free models of regular theories and free models of …

Authors:
Joshua Meyers, David I. Spivak, Ryan Wisnesky

Open Access 07-06-2022

A Comprehensive Framework for Saturation Theorem Proving

A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of …

Authors:
Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette

Open Access 26-05-2022

A Formalization of the Smith Normal Form in Higher-Order Logic

This work presents formal correctness proofs in Isabelle/HOL of algorithms to transform a matrix into Smith normal form, a canonical matrix form, in a general setting: the algorithms are written in an abstract form and parameterized by very few …

Authors:
Jose Divasón, René Thiemann

Open Access 24-05-2022

Set of Support, Demodulation, Paramodulation: A Historical Perspective

This article is a tribute to the scientific legacy of automated reasoning pioneer and JAR founder Lawrence T. (Larry) Wos. Larry’s main technical contributions were the set-of-support strategy for resolution theorem proving, and the demodulation …

Author:
Maria Paola Bonacina

Open Access 23-05-2022

Local is Best: Efficient Reductions to Modal Logic K

We present novel reductions of extensions of the basic modal logic $${\textsf {K} }$$ K with axioms $$\textsf {B} $$ B , $$\textsf {D} $$ D , $$\textsf {T} $$ T , $$\textsf {4} $$ 4 and $$\textsf {5} $$ 5 to Separated Normal Form with Sets of …

Authors:
Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt, Clare Dixon

20-05-2022

Theorem Proving as Constraint Solving with Coherent Logic

In contrast to common automated theorem proving approaches, in which the search space is a set of some formulae and what is sought is again a (goal) formula, we propose an approach based on searching for a proof (of a given length) as a whole.

Authors:
Predrag Janičić, Julien Narboux

Open Access 20-03-2022

Verifying Whiley Programs with Boogie

The quest to develop increasingly sophisticated verification systems continues unabated. Tools such as Dafny, Spec#, ESC/Java, SPARK Ada and Whiley attempt to seamlessly integrate specification and verification into a programming language, in a …

Authors:
David J. Pearce, Mark Utting, Lindsay Groves

28-02-2022

Larry Wos: Visions of Automated Reasoning

This paper celebrates the scientific discoveries and the service to the automated reasoning community of Lawrence (Larry) T. Wos, who passed away in August 2020. The narrative covers Larry’s most long-lasting ideas about inference rules and search …

Authors:
Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe

Open Access 01-02-2022

A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

Shortly before Larry Wos passed away, he sent a manuscript for discussion to Sophie Tourret, the editor of the AAR newsletter. We present excerpts from this final manuscript, put it in its historic context and explain its relevance for today’s …

Authors:
Sophie Tourret, Christoph Weidenbach

30-01-2022

Formalization of the Computational Theory of a Turing Complete Functional Language Model

This work presents a formalization in PVS of the computational theory for a computational model given as a class of partial recursive functions called PVS0. The model is built over basic operators, which, when restricted to constants, successor …

Authors:
Thiago Mendonça Ferreira Ramos, Ariane Alves Almeida, Mauricio Ayala-Rincón