Automatically Deriving Schematic Theorems for Dynamic Contexts

Olivier Savary Bélanger 1 Kaustuv Chaudhuri 2
2 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 : Hypothetical judgments go hand-in-hand with higher-order abstract syntax for meta-theoretic reasoning. Such judgments have two kinds of assumptions: those that are statically known from the specification, and the dynamic assumptions that result from building derivations out of the specification clauses. These dynamic assumptions often have a simple regular structure of repetitions of blocks of related assumptions, with each block generally involving one or several variables and their properties, that are added to the context in a single backchaining step. Reflecting on this regular structure can let us derive a number of structural properties about the elements of the context. We present an extension of the Abella theorem prover, which is based on a simply typed intuitionistic reasoning logic supporting (co-)inductive definitions and generic quantification. Dynamic contexts are repre-sented in Abella using lists of formulas for the assumptions and quantifier nesting for the variables, together with an inductively defined context relation that specifies their structure. We add a new mechanism for defining particular kinds of regular context relations, called schemas, and tacticals to derive theorems from these schemas as needed. Importantly, our extension leaves the trusted kernel of Abella unchanged. We show that these tacticals can eliminate many commonly encountered kinds of administrative lemmas that would otherwise have to be proven manually, which is a common source of complaints from Abella users.
Type de document :
Communication dans un congrès
Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2014, Vienna, Austria. ACM-SIGPLAN, 2014, 〈http://complogic.cs.mcgill.ca/lfmtp14/〉. 〈10.1145/2631172.2631181 〉
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-01091555
Contributeur : Kaustuv Chaudhuri <>
Soumis le : vendredi 5 décembre 2014 - 16:05:44
Dernière modification le : jeudi 10 mai 2018 - 02:06:38
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:04:28

Fichiers

lfmtp14-hal.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Collections

Citation

Olivier Savary Bélanger, Kaustuv Chaudhuri. Automatically Deriving Schematic Theorems for Dynamic Contexts. Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2014, Vienna, Austria. ACM-SIGPLAN, 2014, 〈http://complogic.cs.mcgill.ca/lfmtp14/〉. 〈10.1145/2631172.2631181 〉. 〈hal-01091555〉

Partager

Métriques

Consultations de la notice

454

Téléchargements de fichiers

79