# Logic/General logic/Mechanization of proofs

## Subject Classification

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

## 2024

## 2023

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

by Martin Desharnais

## 2022

##### A Sequent Calculus Prover for First-Order Logic with Functions

by Asta Halkjær From and Frederik Krogsdal Jacobsen

## 2020

##### Extensions to the Comprehensive Framework for Saturation Theorem Proving

by Jasmin Christian Blanchette and Sophie Tourret

## 2019

## 2018

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

by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

##### Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

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

## 2017

##### First-Order Logic According to Harrison

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

## 2016

## 2014

## 2013

##### Sound and Complete Sort Encodings for First-Order Logic

by Jasmin Christian Blanchette and Andrei Popescu

## 2004

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

by Tom Ridge