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.
Type de document :
Communication dans un congrès
4th Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienna, Austria. Konev, Boris and de Moura, Leonardo and Schulz, Stephan. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01101057
Contributeur : Simon Cruanes <>
Soumis le : mardi 13 janvier 2015 - 15:39:52
Dernière modification le : mercredi 14 décembre 2016 - 01:06:49
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 06:39:48

Fichier

logtk_paar.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. Konev, Boris and de Moura, Leonardo and Schulz, Stephan. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. 〈hal-01101057〉

Partager

Métriques

Consultations de
la notice

168

Téléchargements du document

96