package coq-propcalc

  1. Overview
  2. No Docs
Propositional Calculus

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. F
    Floris van Doorn <fpvdoorn@gmail.com>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=2043cc3cb1336535a92fc3a26379d50d

Description

Formalization of basic theorems about classical propositional logic. The main theorems are (1) the soundness and completeness of natural deduction calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus. Keywords: propositional calculus, classical logic, completeness, natural deduction, sequent calculus, cut elimination.

Tags

keyword:propositional calculus keyword:classical logic keyword:completeness keyword:natural deduction keyword:sequent calculus keyword:cut elimination category:Mathematics/Logic/Foundations

Published: 07 Jun 2016

Dependencies (2)

  1. coq >= "8.5" & < "8.6~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None