Logtk : A Logic ToolKit for Automated Reasoning and its Implementation

Simon Cruanes 1
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Paris-Rocquencourt
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 : vendredi 25 mai 2018 - 12:02:06
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

INRIA | INRIA-ROCQ

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

228

Téléchargements de fichiers

172

Contact


archive-ouverte@inria.fr