Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
Author: Simon Cruanes
Paper Information
| Title: | Logtk : A Logic ToolKit for Automated Reasoning and its Implementation |
| Authors: | Simon Cruanes |
| Proceedings: | PAAR 2014 Proceedings |
| Editors: | Stephan Schulz, Leonardo De Moura and Boris Konev |
| Keywords: | OCaml, unification, term representation, discrimination tree, substitution, De Bruijn |
| 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 and algorithms to represent terms, formulas, substitutions, perform unification, index terms, parse problems, as well as a few tools to demonstrate itsuse. It is the basis of a full-fledged superposition prover. |
| Pages: | 11 |
| Talk: | Jul 23 15:00 |
| Paper: |  |