文章基本信息

标题：Abella: A System for Reasoning about Relational Specifications
本地全文：下载
作者：David Baelde ; Kaustuv Chaudhuri ; Andrew Gacek 等
期刊名称：Journal of Formalized Reasoning
印刷版ISSN：1972-5787
出版年度：2014
卷号：7
期号：2
页码：1-89
DOI：10.6092/issn.1972-5787/4650
语种：English
出版社：Alma Mater Studiorum - University of Bologna
摘要：The Abella interactive theorem prover is based on an intuitionistic logic that allows for inductive and co-inductive reasoning over relations. Abella supports the λ-tree approach to treating syntax containing binders: it allows simply typed λ-terms to be used to represent such syntax and it provides higher-order (pattern) unification, the nabla quantifier, and nominal constants for reasoning about these representations. As such, it is a suitable vehicle for formalizing the meta-theory of formal systems such as logics and programming languages. This tutorial exposes Abella incrementally, starting with its capabilities at a first-order logic level and gradually presenting more sophisticated features, ending with the support it offers to the two-level logic approach to meta-theoretic reasoning. Along the way, we show how Abella can be used prove theorems involving natural numbers, lists, and automata, as well as involving typed and untyped λ-calculi and the π-calculus.