Clone wiki

IsaFoL / Home

IsaFoL: Isabelle Formalization of Logic

This repository contains various ongoing Isabelle formalizations of logical calculi.

The goal is to develop lemma libraries and methodology for formalizing modern research in automated reasoning. Our initial focus is on well-established ground and first-order calculi, such as DPLL, CDCL, and resolution. One of our inspirations is the IsaFoR/CeTA project (Isabelle/HOL Formalization of Rewriting for Certified Termination Analysis) at Universität Innsbruck.

Entries

A Variant of the Superposition Calculus

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

Abstract Completeness

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

Abstract Soundness

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

First-Order Logic According to Berghofer (ongoing)

  • Latest version (compatible with Isabelle2016-1): IsaFoL entry

First-Order Logic According to Harrison

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry
  • Variants (compatible with latest Isabelle release): IsaFoL entry

First-Order Logic According to Monk (ongoing)

  • Latest version (compatible with Isabelle2016-1): IsaFoL entry

GRAT Checker

  • Latest version (compatible with Isabelle2016-1): IsaFoL entry

Lambda-Free Higher-Order Knuth-Bendix Orders

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

Lambda-Free Higher-Order Recursive Path Orders

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

Ordered Resolution Prover According to Bachmair & Ganzinger (ongoing)

Paraconsistency

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

Proof Systems for Propositional Logic

Propositional Resolution and Prime Implicates Generation

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

Simple Prover

  • Latest version (compatible with latest Isabelle release): IsaFoL entry

Sound and Complete Sort Encodings for First-Order Logic

  • Latest version (compatible with latest Isabelle repository): AFP entry
  • Recent version (compatible with latest Isabelle release): AFP entry

Unordered Resolution

Weidenbach's Book (ongoing)

Authors

Additional Collaborators

Publications

Updated