Logic

Subject Classification

ACM: Theory of computation~Logic

AMS: Mathematical logic and foundations

2023

A Verified Efficient Implementation of the Weighted Path Order

by René Thiemann and Elias Wenninger

Jun 01

MLSS Decision Procedure

by Lukas Stevens

May 05

MLSS Decision Procedure

by Lukas Stevens

May 05

MLSS Decision Procedure

by Lukas Stevens

May 05

The Halting Problem is Soluble in Malament-Hogarth Spacetimes

by Mike Stannett

Apr 29

A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic

by Martin Desharnais

Apr 20

A Sound and Complete Calculus for Probability Inequalities

by Matthew Doty

Feb 20

A Sound and Complete Calculus for Probability Inequalities

by Matthew Doty

Feb 20

Given Clause Loops

by Jasmin Christian Blanchette, Qi Qiu and Sophie Tourret

Jan 25

Suppes' Theorem For Probability Logic

by Matthew Doty

Jan 22

Synthetic Completeness

by Asta Halkjær From

Jan 09

Synthetic Completeness

by Asta Halkjær From

Jan 09

The Cook-Levin theorem

by Frank J. Balbach

Jan 08

2022

Class-based Classical Propositional Logic

by Matthew Doty

Dec 15

Class-based Classical Propositional Logic

by Matthew Doty

Dec 15

Automation of Boolos' Curious Inference in Isabelle/HOL

by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe

Dec 05

Automation of Boolos' Curious Inference in Isabelle/HOL

by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe

Dec 05

Automation of Boolos' Curious Inference in Isabelle/HOL

by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe

Dec 05

Automation of Boolos' Curious Inference in Isabelle/HOL

by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe

Dec 05

Automation of Boolos' Curious Inference in Isabelle/HOL

by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe

Dec 05

A Verified Translation of Multitape Turing Machines into Singletape Turing Machines

by Christian Dalvit and René Thiemann

Nov 30

Abstract Object Theory

by Daniel Kirchner

Nov 28

Making Arbitrary Relational Calculus Queries Safe-Range

by Martin Raszyk and Dmitriy Traytel

Sep 28

Stalnaker's Epistemic Logic

by Laura P. Gamboa Guzman

Sep 23

Soundness and Completeness of Implicational Logic

by Asta Halkjær From and Jørgen Villadsen

Sep 13

Soundness and Completeness of Implicational Logic

by Asta Halkjær From and Jørgen Villadsen

Sep 13

Boolos's Curious Inference in Isabelle/HOL

by Jeffrey Ketland

Jun 20

Diophantine Equations and the DPRM Theorem

by Jonas Bayer, Marco David, Benedikt Stock, Abhik Pal, Yuri Matiyasevich and Dierk Schleicher

Jun 06

Reducing Rewrite Properties to Properties on Ground Terms

by Alexander Lochmann

Jun 02

The Generalized Multiset Ordering is NP-Complete

by René Thiemann and Lukas Schmidinger

Apr 20

Ackermann's Function Is Not Primitive Recursive

by Lawrence C. Paulson

Mar 23

A Naive Prover for First-Order Logic

by Asta Halkjær From

Mar 22

A Naive Prover for First-Order Logic

by Asta Halkjær From

Mar 22

A Naive Prover for First-Order Logic

by Asta Halkjær From

Mar 22

The Independence of the Continuum Hypothesis in Isabelle/ZF

by Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf and Matías Steinberg

Mar 06

Transitive Models of Fragments of ZFC

by Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf and Matías Steinberg

Mar 03

Wetzel's Problem and the Continuum Hypothesis

by Lawrence C. Paulson

Feb 18

First-Order Query Evaluation

by Martin Raszyk

Feb 15

First-Order Theory of Rewriting

by Alexander Lochmann and Bertram Felgenhauer

Feb 02

First-Order Theory of Rewriting

by Alexander Lochmann and Bertram Felgenhauer

Feb 02

A Sequent Calculus Prover for First-Order Logic with Functions

by Asta Halkjær From and Frederik Krogsdal Jacobsen

Jan 31

A Sequent Calculus Prover for First-Order Logic with Functions

by Asta Halkjær From and Frederik Krogsdal Jacobsen

Jan 31

A Sequent Calculus Prover for First-Order Logic with Functions

by Asta Halkjær From and Frederik Krogsdal Jacobsen

Jan 31

2021

Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL

by Christoph Benzmüller

Nov 08

Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL

by Christoph Benzmüller

Nov 08

Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL

by Christoph Benzmüller and Sebastian Reiche

Nov 08

Belief Revision Theory

by Valentin Fouillard, Safouan Taha, Frédéric Boulanger and Nicolas Sabouret

Oct 19

Soundness and Completeness of an Axiomatic System for First-Order Logic

by Asta Halkjær From

Sep 24

Soundness and Completeness of an Axiomatic System for First-Order Logic

by Asta Halkjær From

Sep 24

A Formalization of Weighted Path Orders and Recursive Path Orders

by Christian Sternagel, René Thiemann and Akihisa Yamada

Sep 16

Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories

by Mihails Milehins

Sep 06

Public Announcement Logic

by Asta Halkjær From

Jun 17

Isabelle's Metalogic: Formalization and Proof Checker

by Tobias Nipkow and Simon Roßkopf

Apr 27

Mereology

Mar 01

Solution to the xkcd Blue Eyes puzzle

by Maya Kądziołka

Jan 30

2020

Cofinality and the Delta System Lemma

by Pedro Sánchez Terraf

Dec 27

Topological semantics for paraconsistent and paracomplete logics

by David Fuenmayor

Dec 17

Syntax-Independent Logic Infrastructure

by Andrei Popescu and Dmitriy Traytel

Sep 16

Robinson Arithmetic

by Andrei Popescu and Dmitriy Traytel

Sep 16

From Abstract to Concrete Gödel's Incompleteness Theorems—Part II

by Andrei Popescu and Dmitriy Traytel

Sep 16

From Abstract to Concrete Gödel's Incompleteness Theorems—Part I

by Andrei Popescu and Dmitriy Traytel

Sep 16

An Abstract Formalization of Gödel's Incompleteness Theorems

by Andrei Popescu and Dmitriy Traytel

Sep 16

Some classical results in inductive inference of recursive functions

by Frank J. Balbach

Aug 31

Extensions to the Comprehensive Framework for Saturation Theorem Proving

by Jasmin Christian Blanchette and Sophie Tourret

Aug 25

Ordinal Partitions

by Lawrence C. Paulson

Aug 03

A Formalization of Knuth–Bendix Orders

by Christian Sternagel and René Thiemann

May 13

Recursion Theorem in ZF

by Georgy Dunaev

May 11

An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation

by Salomon Sickert

May 08

Formalization of Forcing in Isabelle/ZF

by Emmanuel Gunther, Miguel Pagano and Pedro Sánchez Terraf

May 06

Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations

by Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider and Dmitriy Traytel

Apr 09

A Comprehensive Framework for Saturation Theorem Proving

by Sophie Tourret

Apr 09

Implementing the Goodstein Function in λ-Calculus

by Bertram Felgenhauer

Feb 21

2019

Formalizing a Seligman-Style Tableau System for Hybrid Logic

by Asta Halkjær From

Dec 20

Zermelo Fraenkel Set Theory in Higher-Order Logic

by Lawrence C. Paulson

Oct 24

Aristotle's Assertoric Syllogistic

by Angeliki Koutsoukou-Argyraki

Oct 08

A Sequent Calculus for First-Order Logic

by Asta Halkjær From

Jul 18

A Verified Code Generator from Isabelle/HOL to CakeML

Jul 08

Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic

by Joshua Schneider and Dmitriy Traytel

Jul 04

A General Theory of Syntax with Bindings

by Lorenzo Gheri and Andrei Popescu

Apr 06

Universal Turing Machine

by Jian Xu, Xingyuan Zhang, Christian Urban, Sebastiaan J. C. Joosten and Franz Regensburger

Feb 08

2018

Graph Saturation

by Sebastiaan J. C. Joosten

Nov 23

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover

by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

Nov 23

Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL

by David Fuenmayor and Christoph Benzmüller

Oct 30

Epistemic Logic: Completeness of Modal Logics

by Asta Halkjær From

Oct 29

Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms

by Alexander Bentkamp

Oct 19

Minsky Machines

by Bertram Felgenhauer

Aug 14

First-Order Terms

by Christian Sternagel and René Thiemann

Feb 06

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

by Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann

Jan 18

2017

Hybrid Multi-Lane Spatial Logic

Nov 06

Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument

by David Fuenmayor and Christoph Benzmüller

Sep 21

Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL

by Daniel Kirchner

Sep 17

Anselm's God in Isabelle/HOL

Sep 06

Propositional Proof Systems

by Julius Michaelis and Tobias Nipkow

Jun 21

Monad normalisation

by Joshua Schneider, Manuel Eberl and Andreas Lochbihler

May 05

Types, Tableaus and Gödel’s God in Isabelle/HOL

by David Fuenmayor and Christoph Benzmüller

May 01

Differential Dynamic Logic

Feb 13

Abstract Soundness

by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel

Feb 10

First-Order Logic According to Harrison

by Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen

Jan 01

2016

Paraconsistency

by Anders Schlichtkrull and Jørgen Villadsen

Dec 07

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel

Nov 12

Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms

by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

Nov 12

Modal Logics for Nominal Transition Systems

by Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström and Ramunas Gutkovas

Oct 25

Allen's Interval Calculus

by Fadoua Ghourabi

Sep 29

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms

by Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

Sep 23

A Variant of the Superposition Calculus

by Nicolas Peltier

Sep 06

Surprise Paradox

by Joachim Breitner

Jul 17

The Z Property

by Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel

Jun 30

The Resolution Calculus for First-Order Logic

by Anders Schlichtkrull

Jun 30

The meta theory of the Incredible Proof Machine

by Joachim Breitner and Denis Lohner

May 20

Propositional Resolution and Prime Implicates Generation

by Nicolas Peltier

Mar 11

Linear Temporal Logic

by Salomon Sickert

Mar 01

2015

Decreasing Diagrams II

by Bertram Felgenhauer

Aug 20

Derivatives of Logical Formulas

by Dmitriy Traytel

May 28

2014

Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

by Dmitriy Traytel and Tobias Nipkow

Jun 12

Boolean Expression Checkers

by Tobias Nipkow

Jun 08

Abstract Completeness

by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel

Apr 16

A shallow embedding of HyperCTL*

by Markus N. Rabe, Peter Lammich and Andrei Popescu

Apr 16

2013

The Hereditarily Finite Sets

by Lawrence C. Paulson

Nov 17

Gödel's Incompleteness Theorems

by Lawrence C. Paulson

Nov 17

Gödel's God in Isabelle/HOL

by Christoph Benzmüller and Bruno Woltzenlogel Paleo

Nov 12

Decreasing Diagrams

by Harald Zankl

Nov 01

Sound and Complete Sort Encodings for First-Order Logic

by Jasmin Christian Blanchette and Andrei Popescu

Jun 27

2011

Interval Temporal Logic on Natural Numbers

by David Trachtenherz

Feb 23

2010

Abstract Rewriting

by Christian Sternagel and René Thiemann

Jun 14

Free Boolean Algebra

by Brian Huffman

Mar 29

2009

Formalizing the Logic-Automaton Connection

by Stefan Berghofer and Markus Reiter

Dec 03

Ordinals and Cardinals

by Andrei Popescu

Sep 01

Invertibility in Sequent Calculi

by Peter Chapman

Aug 28

2008

Recursion Theory I

by Michael Nedzelsky

Apr 05

Quantifier Elimination for Linear Arithmetic

by Tobias Nipkow

Jan 11

2007

First-Order Logic According to Fitting

by Stefan Berghofer

Aug 02

2005

Countable Ordinals

by Brian Huffman

Nov 11

2004

A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic

Sep 28

Completeness theorem

by James Margetson and Tom Ridge

Sep 20