Logtk : A Logic ToolKit for Automated Reasoning and its Implementation - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Logtk : A Logic ToolKit for Automated Reasoning and its Implementation

Résumé

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.
Fichier principal
Vignette du fichier
logtk_paar.pdf (346.46 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01101057 , version 1 (13-01-2015)

Identifiants

  • HAL Id : hal-01101057 , version 1

Citer

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⟩

Collections

INRIA INRIA2
437 Consultations
289 Téléchargements

Partager

Gmail Facebook X LinkedIn More