Filtering Axiom Links for Proof Nets

Abstract : An important problem for proving statements in multimodal categorial grammar is that even when using proof nets — which improve upon proof search in natural deduction and sequent calculus by identifying all equivalent proofs — the number of possible axiom links to consider is still enormous. We will propose several efficient strategies to reduce the number of axiom links and will evaluate the resulting combined strategy against a large number of random, provable Lambek calculus statements and find that we eliminate 97.92% of the planar axiom links which do not correspond to any proof net.
Type de document :
Communication dans un congrès
Formal Grammar 2007, Aug 2007, Dublin, Ireland. 2007
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00413334
Contributeur : Richard Moot <>
Soumis le : jeudi 3 septembre 2009 - 17:31:19
Dernière modification le : samedi 7 avril 2018 - 11:58:01
Document(s) archivé(s) le : mardi 15 juin 2010 - 21:24:51

Fichier

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

Identifiants

  • HAL Id : inria-00413334, version 1

Collections

Citation

Filtering Axiom Links for Proof Nets. Formal Grammar 2007, Aug 2007, Dublin, Ireland. 2007. 〈inria-00413334〉

Partager

Métriques

Consultations de la notice

62

Téléchargements de fichiers

112