Sign in
J. Autom. Reason.
1985
1998
2011
2024
1985
2024
Keyphrases
Publications
volume 68, number 1, 2024
Benjamin Böhm
,
Tomás Peitl
,
Olaf Beyersdorff
Should Decisions in QCDCL Follow Prefix Order?
J. Autom. Reason.
68 (1) (2024)
David Braun
,
Nicolas Magaud
,
Pascal Schreck
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry.
J. Autom. Reason.
68 (1) (2024)
Étienne Payet
Non-termination in Term Rewriting and Logic Programming.
J. Autom. Reason.
68 (1) (2024)
Mnacho Echenim
,
Mehdi Mhalla
A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL.
J. Autom. Reason.
68 (1) (2024)
Florian Faissole
Formally-Verified Round-Off Error Analysis of Runge-Kutta Methods.
J. Autom. Reason.
68 (1) (2024)
volume 67, number 1, 2023
Qinshi Wang
,
Andrew W. Appel
A Solver for Arrays with Concatenation.
J. Autom. Reason.
67 (1) (2023)
Richard Schmoetten
,
Jake E. Palmer
,
Jacques D. Fleuriot
Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL.
J. Autom. Reason.
67 (1) (2023)
Chelsea Edmonds
,
Angeliki Koutsoukou-Argyraki
,
Lawrence C. Paulson
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL.
J. Autom. Reason.
67 (1) (2023)
Pedro Quaresma
,
Pierluigi Graziani
Measuring the Readability of Geometric Proofs: The Area Method Case.
J. Autom. Reason.
67 (1) (2023)
Dominik Kirst
,
Marc Hermes
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq.
J. Autom. Reason.
67 (1) (2023)
Simon Roßkopf
,
Tobias Nipkow
A Formalization and Proof Checker for Isabelle's Metalogic.
J. Autom. Reason.
67 (1) (2023)
Andrew W. Appel
,
Xavier Leroy
Efficient Extensional Binary Tries.
J. Autom. Reason.
67 (1) (2023)
Guido Fiorino
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic.
J. Autom. Reason.
67 (1) (2023)
Mak Andrlon
Finding Normal Binary Floating-Point Factors Efficiently.
J. Autom. Reason.
67 (1) (2023)
Alvaro Velasquez
,
Ismail Alkhouri
,
K. Subramani
,
Piotr Wojciechowski
,
George K. Atia
Optimal Deterministic Controller Synthesis from Steady-State Distributions.
J. Autom. Reason.
67 (1) (2023)
Maria Paola Bonacina
,
Sarah Winkler
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover.
J. Autom. Reason.
67 (1) (2023)
Aaron Windsor
Computer-Aided Constructions of Commafree Codes.
J. Autom. Reason.
67 (1) (2023)
Alexander Bentkamp
,
Jasmin Blanchette
,
Sophie Tourret
,
Petar Vukmirovic
Superposition for Higher-Order Logic.
J. Autom. Reason.
67 (1) (2023)
volume 67, number 2, 2023
Maximiliano Cristiá
,
Guido De Luca
,
Carlos Luna
An Automatically Verified Prototype of the Android Permissions System.
J. Autom. Reason.
67 (2) (2023)
Emre Yolcu
,
Scott Aaronson
,
Marijn J. H. Heule
An Automated Approach to the Collatz Conjecture.
J. Autom. Reason.
67 (2) (2023)
Luís Cruz-Filipe
,
Fabrizio Montesi
,
Marco Peressotti
A Formal Theory of Choreographic Programming.
J. Autom. Reason.
67 (2) (2023)
Aart Middeldorp
,
Alexander Lochmann
,
Fabian Mitterwallner
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification.
J. Autom. Reason.
67 (2) (2023)
Gabriel Ebner
,
Jasmin Blanchette
,
Sophie Tourret
Unifying Splitting.
J. Autom. Reason.
67 (2) (2023)
Alessandro Abate
,
Haniel Barbosa
,
Clark W. Barrett
,
Cristina David
,
Pascal Kesseli
,
Daniel Kroening
,
Elizabeth Polgreen
,
Andrew Reynolds
,
Cesare Tinelli
Synthesising Programs with Non-trivial Constants.
J. Autom. Reason.
67 (2) (2023)
Cezary Kaliszyk
,
Karol Pak
Combining Higher-Order Logic with Set Theory Formalizations.
J. Autom. Reason.
67 (2) (2023)
Oliver Nash
Engel's Theorem in Mathlib.
J. Autom. Reason.
67 (2) (2023)
volume 67, number 3, 2023
Hendrik Leidinger
,
Christoph Weidenbach
SCL(EQ): SCL for First-Order Logic with Equality.
J. Autom. Reason.
67 (3) (2023)
Anupam Das
,
Marianna Girlando
Cyclic Hypersequent System for Transitive Closure Logic.
J. Autom. Reason.
67 (3) (2023)
Mnacho Echenim
,
Nicolas Peltier
A Proof Procedure for Separation Logic with Inductive Definitions and Data.
J. Autom. Reason.
67 (3) (2023)
Ying Sheng
,
Andres Nötzli
,
Andrew Reynolds
,
Yoni Zohar
,
David L. Dill
,
Wolfgang Grieskamp
,
Junkil Park
,
Shaz Qadeer
,
Clark W. Barrett
,
Cesare Tinelli
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences.
J. Autom. Reason.
67 (3) (2023)
Yun-Rong Luo
,
Che Cheng
,
Jie-Hong R. Jiang
A Resolution Proof System for Dependency Stochastic Boolean Satisfiability.
J. Autom. Reason.
67 (3) (2023)
Marco Maggesi
,
Cosimo Perini Brogi
Mechanising Gödel-Löb Provability Logic in HOL Light.
J. Autom. Reason.
67 (3) (2023)
Andrei Popescu
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version.
J. Autom. Reason.
67 (3) (2023)
Reynald Affeldt
,
Cyril Cohen
Measure Construction by Extension in Dependent Type Theory with Application to Integration.
J. Autom. Reason.
67 (3) (2023)
Joseph E. Reeves
,
Marijn J. H. Heule
,
Randal E. Bryant
Preprocessing of Propagation Redundant Clauses.
J. Autom. Reason.
67 (3) (2023)
Christian Urban
POSIX Lexing with Derivatives of Regular Expressions.
J. Autom. Reason.
67 (3) (2023)
Stepan Holub
,
Martin Raska
,
Stepán Starosta
Binary Codes that do not Preserve Primitivity.
J. Autom. Reason.
67 (3) (2023)
volume 67, number 4, 2023
Érik Martin-Dorel
,
Guillaume Melquiond
,
Pierre Roux
Enabling Floating-Point Arithmetic in the Coq Proof Assistant.
J. Autom. Reason.
67 (4) (2023)
Andrzej Indrzejczak
Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation.
J. Autom. Reason.
67 (4) (2023)
Xicheng Peng
,
Jingzhong Zhang
,
Mao Chen
,
Sannyuya Liu
Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity.
J. Autom. Reason.
67 (4) (2023)
Sen Zheng
,
Renate A. Schmidt
Saturation-Based Boolean Conjunctive Query Answering and Rewriting for the Guarded Quantification Fragments.
J. Autom. Reason.
67 (4) (2023)
César A. Muñoz
,
Mauricio Ayala-Rincón
,
Mariano M. Moscato
,
Aaron Dutle
,
Anthony J. Narkawicz
,
Ariane Alves Almeida
,
Andréia B. Avelar da Silva
,
Thiago Mendonça Ferreira Ramos
Formal Verification of Termination Criteria for First-Order Recursive Functions.
J. Autom. Reason.
67 (4) (2023)
Benjamin Böhm
,
Olaf Beyersdorff
Lower Bounds for QCDCL via Formula Gauge.
J. Autom. Reason.
67 (4) (2023)
Philipp G. Haselwarter
,
Andrej Bauer
Finitary Type Theories With and Without Contexts.
J. Autom. Reason.
67 (4) (2023)
Ying Sheng
,
Yoni Zohar
,
Christophe Ringeissen
,
Andrew Reynolds
,
Clark W. Barrett
,
Cesare Tinelli
Combining Stable Infiniteness and (Strong) Politeness.
J. Autom. Reason.
67 (4) (2023)
volume 66, number 4, 2022
Richard Schmoetten
,
Jake E. Palmer
,
Jacques D. Fleuriot
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL.
J. Autom. Reason.
66 (4) (2022)
Mallku Soldevila
,
Beta Ziliani
,
Bruno Silvestre
From Specification to Testing: Semantics Engineering for Lua 5.2.
J. Autom. Reason.
66 (4) (2022)
Fabio Papacchini
,
Cláudia Nalon
,
Ullrich Hustadt
,
Clare Dixon
Local is Best: Efficient Reductions to Modal Logic K.
J. Autom. Reason.
66 (4) (2022)
Jose Divasón
,
René Thiemann
A Formalization of the Smith Normal Form in Higher-Order Logic.
J. Autom. Reason.
66 (4) (2022)
Sophie Tourret
,
Christoph Weidenbach
A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column.
J. Autom. Reason.
66 (4) (2022)