Flexary Operators for Formalized Mathematics

DOI10.1007/978-3-319-08434-3_23zbMath1304.68171OpenAlexW126695022WikidataQ57389322 ScholiaQ57389322MaRDI QIDQ5495932

Michael Kohlhase, Florian Rabe, Fulya Horozal

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08434-3_23

Mathematics Subject Classification ID

Knowledge representation (68T30)

Related Items (6)

Formal Logic Definitions for Interchange Languages ⋮ Readable Formalization of Euler’s Partition Theorem in Mizar ⋮ Injecting formal mathematics into LaTeX ⋮ Flexary connectives in Mizar ⋮ Variadic equational matching in associative and commutative theories ⋮ Towards Knowledge Management for HOL Light

Uses Software

• Coq
• Isabelle
• Mathematica
• Twelf
• MMT
• QMT
• MathML

Cites Work

• Unnamed Item
• A scalable module system
• The calculus of constructions
• Isabelle. A generic theorem prover
• The MMT API: A Generic MKM System
• Tentative Experiments with Ellipsis in Mizar
• A framework for defining logics
• Mathematical Knowledge Management
• Mathematical Knowledge Management

This page was built for publication: Flexary Operators for Formalized Mathematics