Found 2 Possible Name Variants:

Document

**Published in:** LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Systems in which classical and intuitionistic logics coexist are called ecumenical. Such a system allows for interoperability and hybridization between classical and constructive propositions and proofs. We study Ecumenical STT, a theory expressed in the logical framework of the λΠ-calculus modulo theory. We prove soudness and conservativity of four subtheories of Ecumenical STT with respect to constructive and classical predicate logic and simple type theory. We also prove the weak normalization of well-typed terms and thus the consistency of Ecumenical STT.

Emilie Grienenberger. Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{grienenberger:LIPIcs.TYPES.2022.4, author = {Grienenberger, Emilie}, title = {{Expressing Ecumenical Systems in the \lambda\Pi-Calculus Modulo Theory}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.4}, URN = {urn:nbn:de:0030-drops-184479}, doi = {10.4230/LIPIcs.TYPES.2022.4}, annote = {Keywords: dependent types, predicate logic, higher order logic, constructivism, interoperability, ecumenical logics} }

Document

**Published in:** LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20, author = {Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois}, title = {{Some Axioms for Mathematics}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {20:1--20:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.20}, URN = {urn:nbn:de:0030-drops-142581}, doi = {10.4230/LIPIcs.FSCD.2021.20}, annote = {Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty} }

Document

**Published in:** LIPIcs, Volume 127, 22nd International Conference on Database Theory (ICDT 2019)

We study the problem of learning properties of nodes in tree structures. Those properties are specified by logical formulas, such as formulas from first-order or monadic second-order logic. We think of the tree as a database encoding a large dataset and therefore aim for learning algorithms which depend at most sublinearly on the size of the tree. We present a learning algorithm for quantifier-free formulas where the running time only depends polynomially on the number of training examples, but not on the size of the background structure. By a previous result on strings we know that for general first-order or monadic second-order (MSO) formulas a sublinear running time cannot be achieved. However, we show that by building an index on the tree in a linear time preprocessing phase, we can achieve a learning algorithm for MSO formulas with a logarithmic learning phase.

Emilie Grienenberger and Martin Ritzert. Learning Definable Hypotheses on Trees. In 22nd International Conference on Database Theory (ICDT 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 127, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{grienenberger_et_al:LIPIcs.ICDT.2019.24, author = {Grienenberger, Emilie and Ritzert, Martin}, title = {{Learning Definable Hypotheses on Trees}}, booktitle = {22nd International Conference on Database Theory (ICDT 2019)}, pages = {24:1--24:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-101-6}, ISSN = {1868-8969}, year = {2019}, volume = {127}, editor = {Barcelo, Pablo and Calautti, Marco}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2019.24}, URN = {urn:nbn:de:0030-drops-103261}, doi = {10.4230/LIPIcs.ICDT.2019.24}, annote = {Keywords: monadic second-order logic, trees, query learning} }

Document

**Published in:** LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Systems in which classical and intuitionistic logics coexist are called ecumenical. Such a system allows for interoperability and hybridization between classical and constructive propositions and proofs. We study Ecumenical STT, a theory expressed in the logical framework of the λΠ-calculus modulo theory. We prove soudness and conservativity of four subtheories of Ecumenical STT with respect to constructive and classical predicate logic and simple type theory. We also prove the weak normalization of well-typed terms and thus the consistency of Ecumenical STT.

Emilie Grienenberger. Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{grienenberger:LIPIcs.TYPES.2022.4, author = {Grienenberger, Emilie}, title = {{Expressing Ecumenical Systems in the \lambda\Pi-Calculus Modulo Theory}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.4}, URN = {urn:nbn:de:0030-drops-184479}, doi = {10.4230/LIPIcs.TYPES.2022.4}, annote = {Keywords: dependent types, predicate logic, higher order logic, constructivism, interoperability, ecumenical logics} }

Document

**Published in:** LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{blanqui_et_al:LIPIcs.FSCD.2021.20, author = {Blanqui, Fr\'{e}d\'{e}ric and Dowek, Gilles and Grienenberger, \'{E}milie and Hondet, Gabriel and Thir\'{e}, Fran\c{c}ois}, title = {{Some Axioms for Mathematics}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {20:1--20:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.20}, URN = {urn:nbn:de:0030-drops-142581}, doi = {10.4230/LIPIcs.FSCD.2021.20}, annote = {Keywords: logical framework, axiomatic theory, dependent types, rewriting, interoperabilty} }

Document

**Published in:** LIPIcs, Volume 127, 22nd International Conference on Database Theory (ICDT 2019)

We study the problem of learning properties of nodes in tree structures. Those properties are specified by logical formulas, such as formulas from first-order or monadic second-order logic. We think of the tree as a database encoding a large dataset and therefore aim for learning algorithms which depend at most sublinearly on the size of the tree. We present a learning algorithm for quantifier-free formulas where the running time only depends polynomially on the number of training examples, but not on the size of the background structure. By a previous result on strings we know that for general first-order or monadic second-order (MSO) formulas a sublinear running time cannot be achieved. However, we show that by building an index on the tree in a linear time preprocessing phase, we can achieve a learning algorithm for MSO formulas with a logarithmic learning phase.

Emilie Grienenberger and Martin Ritzert. Learning Definable Hypotheses on Trees. In 22nd International Conference on Database Theory (ICDT 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 127, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{grienenberger_et_al:LIPIcs.ICDT.2019.24, author = {Grienenberger, Emilie and Ritzert, Martin}, title = {{Learning Definable Hypotheses on Trees}}, booktitle = {22nd International Conference on Database Theory (ICDT 2019)}, pages = {24:1--24:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-101-6}, ISSN = {1868-8969}, year = {2019}, volume = {127}, editor = {Barcelo, Pablo and Calautti, Marco}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2019.24}, URN = {urn:nbn:de:0030-drops-103261}, doi = {10.4230/LIPIcs.ICDT.2019.24}, annote = {Keywords: monadic second-order logic, trees, query learning} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail