Logtk : A Logic ToolKit for Automated Reasoning and its Implementation

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01101057
Contributor : Simon Cruanes <>
Submitted on : Tuesday, January 13, 2015 - 3:39:52 PM
Last modification on : Friday, May 25, 2018 - 12:02:06 PM
Long-term archiving on : Friday, September 11, 2015 - 6:39:48 AM

File

logtk_paar.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01101057, version 1

Collections

Citation

Simon Cruanes. Logtk : A Logic ToolKit for Automated Reasoning and its Implementation. 4th Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienna, Austria. ⟨hal-01101057⟩

Share

Metrics

Record views

277

Files downloads

267