Subformula Linking as an Interaction Method

Kaustuv Chaudhuri 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Current techniques for building formal proofs interactively involve one or several proof languages for instructing an interpreter of the languages to build or check the proof being described. These linguistic approaches have a drawback: the languages are not generally portable, even though the nature of logical reasoning is universal. We propose a somewhat speculative alternative method that lets the user directly manipulate the text of the theorem, using non-linguistic metaphors. It uses a proof formalism based on linking subformulas, which is a variant of deep inference (inference rules are allowed to apply in any formula context) where the relevant formulas in a rule are allowed to be arbitrarily distant. We substantiate the design with a prototype implementation of a linking-based interactive prover for first-order classical linear logic.
Type de document :
Communication dans un congrès
4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.386-401, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_28〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00937009
Contributeur : Kaustuv Chaudhuri <>
Soumis le : lundi 27 janvier 2014 - 16:33:06
Dernière modification le : jeudi 12 avril 2018 - 01:47:08
Document(s) archivé(s) le : dimanche 27 avril 2014 - 23:16:29

Fichiers

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

Identifiants

Collections

Citation

Kaustuv Chaudhuri. Subformula Linking as an Interaction Method. 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.386-401, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_28〉. 〈hal-00937009〉

Partager

Métriques

Consultations de la notice

331

Téléchargements de fichiers

93