First_Order_Terms Dependents

2024

Undecidability Results on Orienting Single Rewrite Rules

by René Thiemann, Fabian Mitterwallner and Aart Middeldorp

Apr 25

2023

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

by Martin Desharnais

Apr 20

2020

Extensions to the Comprehensive Framework for Saturation Theorem Proving

by Jasmin Christian Blanchette and Sophie Tourret

Aug 25

A Formalization of Knuth–Bendix Orders

by Christian Sternagel and René Thiemann

May 13

Stateful Protocol Composition and Typing

by Andreas V. Hess, Sebastian Mödersheim and Achim D. Brucker

Apr 08

2018

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

by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

Nov 23

2016

The Resolution Calculus for First-Order Logic

by Anders Schlichtkrull

Jun 30