Journal of Automated Reasoning 1/2023

Open Access 01.03.2023

A Formalization and Proof Checker for Isabelle’s Metalogic

Simon Roßkopf, Tobias Nipkow

PDF-Version jetzt herunterladen Zum Volltext

Open Access 01.03.2023

Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL

Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson

PDF-Version jetzt herunterladen Zum Volltext

01.03.2023

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

Guido Fiorino

01.03.2023

A Solver for Arrays with Concatenation

Qinshi Wang, Andrew W. Appel

Open Access 01.03.2023

Measuring the Readability of Geometric Proofs: The Area Method Case

Pedro Quaresma, Pierluigi Graziani

PDF-Version jetzt herunterladen Zum Volltext

01.03.2023

Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover

Maria Paola Bonacina, Sarah Winkler

01.03.2023

Optimal Deterministic Controller Synthesis from Steady-State Distributions

Alvaro Velasquez, Ismail Alkhouri, K. Subramani, Piotr Wojciechowski, George Atia

01.03.2023

Efficient Extensional Binary Tries

Andrew W. Appel, Xavier Leroy

Open Access 01.03.2023 | Correction

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

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

PDF-Version jetzt herunterladen Zum Volltext

01.03.2023

Superposition for Higher-Order Logic

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović

Open Access 01.03.2023

Finding Normal Binary Floating-Point Factors Efficiently

Mak Andrlon

PDF-Version jetzt herunterladen Zum Volltext

01.03.2023

Computer-Aided Constructions of Commafree Codes

Aaron A. Windsor

Open Access 01.03.2023

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

Extended Version

Dominik Kirst, Marc Hermes

PDF-Version jetzt herunterladen Zum Volltext

Springer Professional

Journal of Automated Reasoning

Ausgabe 1/2023

Inhaltsverzeichnis (13 Artikel)

A Formalization and Proof Checker for Isabelle’s Metalogic

Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

A Solver for Arrays with Concatenation

Measuring the Readability of Geometric Proofs: The Area Method Case

Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover

Optimal Deterministic Controller Synthesis from Steady-State Distributions

Efficient Extensional Binary Tries

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

Superposition for Higher-Order Logic

Finding Normal Binary Floating-Point Factors Efficiently

Computer-Aided Constructions of Commafree Codes

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

Aktuelle Ausgaben

Ausgabe 1/2023

Ausgabe 4/2022

Ausgabe 3/2022

Ausgabe 2/2022

Ausgabe 1/2022

Ausgabe 8/2021

Ausgabe 7/2021

Ausgabe 6/2021

Ausgabe 5/2021

Ausgabe 4/2021

Premium Partner