Skip to main content
main-content

Journal of Automated Reasoning OnlineFirst articles

13.10.2021 Open Access

Proof Complexity of Modal Resolution

We investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods—24th international conference …

12.09.2021 Open Access

Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs

Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform non-trivial inferences only when …

08.04.2019

Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations

In this paper we present a solver for a first-order logic language where sets and binary relations can be freely and naturally combined. The language can express, at least, any full set relation algebra on finite sets. It provides untyped …

01.03.2019 Open Access

Blocking and Other Enhancements for Bottom-Up Model Generation Methods

Model generation is a problem complementary to theorem proving and is important for fault analysis and debugging of formal specifications of security protocols, programs and terminological definitions, for example. This paper discusses several …

11.02.2019

Using Well-Founded Relations for Proving Operational Termination

In this paper, we study operational termination, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different levels by means of well-founded …

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