Logic/General Logic

Subject Classification

AMS: Mathematical logic and foundations / General logic

2023

Suppes' Theorem For Probability Logic

by Matthew Doty

Jan 22

Synthetic Completeness

by Asta Halkjær From

Jan 09

2022

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

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

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

First-Order Query Evaluation

by Martin Raszyk

Feb 15

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

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

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

Solution to the xkcd Blue Eyes puzzle

by Maya Kądziołka

Jan 30

2020

Topological semantics for paraconsistent and paracomplete logics

by David Fuenmayor

Dec 17

Extensions to the Comprehensive Framework for Saturation Theorem Proving

by Jasmin Christian Blanchette and Sophie Tourret

Aug 25

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

by Salomon Sickert

May 08

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

2019

Formalizing a Seligman-Style Tableau System for Hybrid Logic

by Asta Halkjær From

Dec 20

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

2018

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

by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

Nov 23

Epistemic Logic: Completeness of Modal Logics

by Asta Halkjær From

Oct 29

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

by Sven Linker

Nov 06

Differential Dynamic Logic

by Rose Bohrer

Feb 13

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

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

The Resolution Calculus for First-Order Logic

by Anders Schlichtkrull

Jun 30

Propositional Resolution and Prime Implicates Generation

by Nicolas Peltier

Mar 11

Linear Temporal Logic

by Salomon Sickert

Mar 01

2015

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

A shallow embedding of HyperCTL*

by Markus N. Rabe, Peter Lammich and Andrei Popescu

Apr 16

2013

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

Free Boolean Algebra

by Brian Huffman

Mar 29

2009

Formalizing the Logic-Automaton Connection

by Stefan Berghofer and Markus Reiter

Dec 03

2008

Quantifier Elimination for Linear Arithmetic

by Tobias Nipkow

Jan 11

2007

First-Order Logic According to Fitting

by Stefan Berghofer

Aug 02

2004

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

by Tom Ridge

Sep 28