Skip to main content

Journal of Automated Reasoning OnlineFirst articles


Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs. In this paper we give an alternative …


Introduction to Milestones in Interactive Theorem Proving

The special issue’s call for papers began as follows:

The past few decades have seen major achievements in interactive theorem proving, such as the formalization of deep mathematical theorems and significant bodies of theoretical computer science …

23.03.2018 Open Access

On the Generation of Quantified Lemmas

In this paper we present an algorithmic method of lemma introduction. Given a proof in predicate logic with equality the algorithm is capable of introducing several universal lemmas. The method is based on an inversion of Gentzen’s cut-elimination …


Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches

We consider the problem of formally verifying an algorithm in a proof assistant and generating efficient code. Reasoning about correctness is best done at an abstract level, but efficiency of the generated code often requires complicated data …


Formally Verified Approximations of Definite Integrals

Finding an elementary form for an antiderivative is often a difficult task, so numerical integration has become a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made …

Aktuelle Ausgaben

Über diese Zeitschrift

The interdisciplinary Journal of Automated Reasoning balances theory, implementation and application. The spectrum of coverage ranges from the presentation of a new inference rule with proof of its logical properties to a detailed account of a computer program designed to solve various problems in industry. Topics include automated theorem proving, logic programming, expert systems, program synthesis and validation, artificial intelligence, computational logic, robotics, and various industrial applications. The contents focus on several aspects of automated reasoning, a field whose objective is the design and implementation of a computer program that serves as an assistant in solving problems and in answering questions that require reasoning.

The Journal of Automated Reasoning provides a forum and a means for exchanging information for those interested purely in theory, those interested primarily in implementation, and those interested in specific research and industrial applications.

Proof Pearls

In addition to regular research articles, the Journal of Automated Reasoning offers the special article type Proof Pearls. The goal is to disseminate insights gleaned from the growing body of machine-checked formalizations and proofs, obtained using both interactive and automated methods. Application areas include the full range from pure mathematics and logic to software and hardware verification. Proof Pearls should be short communications that focus on a few central ideas rather than extended research reports.

Contributions may include: a short, elegant proof of a self-standing result; a novel way of defining a fundamental concept; a notable approach to proving a key lemma in a larger development; a snippet of verified code, carefully engineered to balance efficiency with ease of verification; or a clever or impressive application of automated tools in a particular domain.

Proof Pearls adapt Jon Bentley's notion of a "programming pearl" to the verification paradigm. Proof Pearls should thus encapsulate fundamental insights that are adaptable and reusable, while being elegant and satisfying in their own right. Typical examples could be a verification of Huffman's algorithm, a perspicuous proof of the fundamental theorem of algebra, or a novel axiomatization of a particular algebraic system that was discovered using automated methods.

Submissions will undergo the usual refereeing process, and will be evaluated according to expository and theoretical merit. Systems and formalizations should be made available online.

Weitere Informationen

Premium Partner

Neuer Inhalt

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.



Safety & Security – Erfolgsfaktoren von sensitiven Robotertechnologien

Forderungen von Industrie 4.0 nach vollständiger Vernetzung der Systeme geben der "Robotersicherheit" einen besonderen Stellenwert: Hierbei umfasst der deutsche Begriff Sicherheit die – im Englischen einerseits durch Safety umrissene physische Sicherheit – sowie andererseits die durch Security definierte informationstechnische Cyber-Sicherheit. Dieser Fachbeitrag aus der e&i beleuchtet eingehend die wesentlichen Aspekte von Safety und Security in der Robotik.
Jetzt gratis downloaden!