Theory morphisms in Church's type theory with quotation and evaluation

DOI10.1007/978-3-319-62075-6_11zbMath1367.68302arXiv1703.02117OpenAlexW2605359050MaRDI QIDQ2364672

William M. Farmer

Publication date: 21 July 2017

Full work available at URL: https://arxiv.org/abs/1703.02117

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Knowledge representation (68T30)

Related Items

Formalizing mathematical knowledge as a biform theory graph: a case study ⋮ Incorporating quotation and evaluation into Church's type theory

Uses Software

• ML
• HOL
• ETPS
• HOL Light

Cites Work

• Unnamed Item
• Mathematical knowledge management: transcending the one-brain-barrier with theory graphs
• An introduction to mathematical logic and type theory: To truth through proof.
• Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics
• The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation
• Andrews' Type Theory with Undefinedness
• HOL Light: An Overview
• Automated Reasoning
• High-Level Theories