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

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