Logic/General logic/Mechanization of proofs

Subject Classification

AMS: Mathematical logic and foundations / General logic / Mechanization of proofs and logical operations

2023

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

by Martin Desharnais

Apr 20

2022

A Naive Prover for First-Order Logic

by Asta Halkjær From

Mar 22

A Sequent Calculus Prover for First-Order Logic with Functions

by Asta Halkjær From and Frederik Krogsdal Jacobsen

Jan 31

2020

Extensions to the Comprehensive Framework for Saturation Theorem Proving

by Jasmin Christian Blanchette and Sophie Tourret

Aug 25

A Comprehensive Framework for Saturation Theorem Proving

by Sophie Tourret

Apr 09

2019

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

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

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

Jan 18

2017

First-Order Logic According to Harrison

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

Jan 01

2016

The Resolution Calculus for First-Order Logic

by Anders Schlichtkrull

Jun 30

Propositional Resolution and Prime Implicates Generation

by Nicolas Peltier

Mar 11

2014

Boolean Expression Checkers

by Tobias Nipkow

Jun 08

2013

Sound and Complete Sort Encodings for First-Order Logic

by Jasmin Christian Blanchette and Andrei Popescu

Jun 27

2004

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

by Tom Ridge

Sep 28