Back to Search
Start Over
Abella: A System for Reasoning about Relational Specifications
- Source :
- Journal of Formalized Reasoning, Journal of Formalized Reasoning, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. ⟨10.6092/issn.1972-5787/4650⟩, Scopus-Elsevier, Journal of Formalized Reasoning, Vol 7, Iss 2, Pp 1-89 (2014), Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. ⟨10.6092/issn.1972-5787/4650⟩
- Publication Year :
- 2014
- Publisher :
- Alma Mater Studiorum - University of Bologna, 2014.
-
Abstract
- 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.<br />Journal of Formalized Reasoning, Vol 7, No 2 (2014): Special Issue: User Tutorials 2
- Subjects :
- ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.1: Computational logic
lcsh:QA801-939
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory
lcsh:Analytic mechanics
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
0102 computer and information sciences
02 engineering and technology
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs
01 natural sciences
lcsh:QA75.5-76.95
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
0202 electrical engineering, electronic engineering, information engineering
lcsh:Electronic computers. Computer science
Subjects
Details
- Language :
- English
- ISSN :
- 19725787
- Database :
- OpenAIRE
- Journal :
- Journal of Formalized Reasoning, Journal of Formalized Reasoning, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. ⟨10.6092/issn.1972-5787/4650⟩, Scopus-Elsevier, Journal of Formalized Reasoning, Vol 7, Iss 2, Pp 1-89 (2014), Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. ⟨10.6092/issn.1972-5787/4650⟩
- Accession number :
- edsair.doi.dedup.....40126f30b6b6c308d3f76f82747dd5d6
- Full Text :
- https://doi.org/10.6092/issn.1972-5787/4650