Zobrazeno 1 - 10
of 11
pro vyhledávání: '"Fulya Horozal"'
Autor:
Florian Rabe, Fulya Horozal
Publikováno v:
LSFA
In a broad sense, logic is the field of formal languages for knowledge and truth that have a formal semantics. It tends to be difficult to give a narrower definition because very different kinds of logics exist. One of the most fundamental contrasts
Autor:
Fulya Horozal, Florian Rabe
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319206141
CICM
CICM
System integration often requires standardized interchange languages, via which systems can exchange mathematical knowledge. Major examples are the MathML-based markup languages and TPTP. However, these languages standardize only the syntax of the ex
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c5ff14a481be172dee2453983509d3a0
https://doi.org/10.1007/978-3-319-20615-8_11
https://doi.org/10.1007/978-3-319-20615-8_11
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319084336
CICM
CICM
We study representation formats that allow formally defining what we call flexary operators: functions that take arbitrarily many arguments, like \(\sum_{k=1}^n a_k\) or binders that bind arbitrarily many variables, like ∀ x1,…x n . F. Concretely
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4094de9cf44dcc98a7bc09946ca1be18
https://doi.org/10.1007/978-3-319-08434-3_23
https://doi.org/10.1007/978-3-319-08434-3_23
Publikováno v:
Recent Trends in Algebraic Development Techniques ISBN: 9783642376344
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::452393286aa1959a3f937630ed329670
https://doi.org/10.1007/978-3-642-37635-1_7
https://doi.org/10.1007/978-3-642-37635-1_7
Autor:
Mihai Codescu, Till Mossakowski, Kristina Sojakova, Florian Rabe, Michael Kohlhase, Fulya Horozal
Publikováno v:
Recent Trends in Algebraic Development Techniques ISBN: 9783642284113
WADT
WADT
LF is a meta-logical framework that has become a standard tool for representing logics and studying their properties. Its focus is proof theoretic, employing the Curry-Howard isomorphism: propositions are represented as types, and proofs as terms. He
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e93d00246f0e24d7261139c450c5a8a5
https://doi.org/10.1007/978-3-642-28412-0_10
https://doi.org/10.1007/978-3-642-28412-0_10
Publikováno v:
Recent Trends in Algebraic Development Techniques ISBN: 9783642284113
WADT
WADT
Logical frameworks like LF are used for formal representations of logics in order to make them amenable to formal machine-assisted meta-reasoning. While the focus has originally been on logics with a proof theoretic semantics, we have recently shown
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::dad2adb91e4bc69721bb5716a84e725d
https://doi.org/10.1007/978-3-642-28412-0_9
https://doi.org/10.1007/978-3-642-28412-0_9
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642313738
AISC/MKM/Calculemus
AISC/MKM/Calculemus
Successful representation and markup languages find a good balance between giving the user freedom of expression, enforcing the fundamental semantic invariants of the modeling framework, and allowing machine support for the underlying semantic struct
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::353c08e4a722d7e92a777999369588f3
https://doi.org/10.1007/978-3-642-31374-5_5
https://doi.org/10.1007/978-3-642-31374-5_5
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642226724
Calculemus/MKM
Calculemus/MKM
LATIN aims at developing methods, techniques, and tools for interfacing logics and related formal systems. These systems are at the core of mathematics and computer science and are implemented in systems like (semi-)automated theorem provers, model c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::77372e0087b93a05c892b0a67ced66a7
https://doi.org/10.1007/978-3-642-22673-1_24
https://doi.org/10.1007/978-3-642-22673-1_24
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642226724
Calculemus/MKM
Calculemus/MKM
In this paper, we try to bridge the gap between different dimensions/ incarnations of mathematical knowledge: MKM representation formats (content), their human-oriented languages (source, presentation), their narrative linearizations (narration), and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a2007a67c17b3e65496e019929633bc5
https://doi.org/10.1007/978-3-642-22673-1_15
https://doi.org/10.1007/978-3-642-22673-1_15
Publikováno v:
Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants.
We present a case study on a modular formal representation of algebra in the recently developed module system for the Twelf implementation of the Edinburgh Logical Framework LF. The module system employs signature morphisms as its main primitive conc