Logtk : A Logic ToolKit for Automated Reasoning and its Implementation | Zendy

Simon Cruanes | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Logtk : A Logic ToolKit for Automated Reasoning and its Implementation

Author(s) -

Simon Cruanes

Publication year - 2018

Publication title -

epic series in computing

Language(s) - English

Resource type - Conference proceedings

ISSN - 2398-7340

DOI - 10.29007/4z1m

Subject(s) - unification , computer science , programming language , gas meter prover , automated theorem proving , automated reasoning , parsing , first order logic , theoretical computer science , mathematics , geometry , mathematical proof

We describe the design and implementation of Logtk, an OCaml library for writing automated reasoning tools that deal with (possibly typed) first-order logic. The library provides data structures to represent terms, formulas and substitutions, and algorithms to index terms, unify them. It also contains parsers and a few tools to demonstrate its use. It is the basis of a full-fledged superposition prover.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research