package logtk

  1. Overview
  2. Docs
On This Page
  1. Low Level Prover
Core types and algorithms for logic

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

2.0.tar.gz
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63

doc/logtk.proofs/Logtk_proofs/LLProver/index.html

Module Logtk_proofs.LLProver

Low Level Prover

A small theorem prover that checks entailment of ground formulas, with higher order terms and some theories

type form = LLTerm.Form.t
type res =
  1. | R_ok
  2. | R_fail
type final_state
val can_check : LLProof.tag list -> bool

Is this set of tags accepted by the tableau prover?

val prove : form list -> form -> res * final_state

prove a b returns R_ok if a => b is a tautology.