Zobrazeno 1 - 6
of 6
pro vyhledávání: '"Daria Walukiewicz-Chrząszcz"'
Publikováno v:
ACM Transactions on Computational Logic. 17:1-29
We show that the constructive predicate logic with positive (covariant) quantification is hard for doubly exponential universal time, that is, for the class co- 2-N exptime . Our approach is to represent proof-search as computation of an alternating
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::733004d2f6260bd510ec85a7676e6911
https://doi.org/10.1145/2981544
https://doi.org/10.1145/2981544
Autor:
Daria Walukiewicz-Chrząszcz
Publikováno v:
Proceedings of the Workshop on Logical Frameworks and Meta-languages (Part of the LICS`2000)
We show how to incorporate rewriting into the Calculus of Constructions and we prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. An important novelty of this paper is the possibility to define rewrit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4ca7e4ee41128578082a6750184c8a10
https://doi.org/10.1017/s0956796802004641
https://doi.org/10.1017/s0956796802004641
Publikováno v:
Interactive Theorem Proving ISBN: 9783642140518
ITP
ITP
Extending the calculus of constructions with rewriting would greatly improve the efficiency of proof assistants such as Coq. In this paper we address the issue of the logical power of such an extension. In our previous work we proposed a procedure to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::aeb613319418b268f339fcbc5e672016
https://doi.org/10.1007/978-3-642-14052-5_31
https://doi.org/10.1007/978-3-642-14052-5_31
Publikováno v:
Automated Reasoning ISBN: 9783540371878
IJCAR
IJCAR
Adding rewriting to a proof assistant based on the Curry-Howard isomorphism, such as Coq, may greatly improve usability of the tool. Unfortunately adding an arbitrary set of rewrite rules may render the underlying formal system undecidable and incons
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8ea43711b045838d21e22be89cd0778f
https://doi.org/10.2168/lmcs-4(3:8)2008
https://doi.org/10.2168/lmcs-4(3:8)2008
Publikováno v:
Rewriting, Computation and Proof ISBN: 9783540731467
Rewriting, Computation and Proof
Rewriting, Computation and Proof
Equational reasoning in Coq is not straightforward. For a few years now there has been an ongoing research process towards adding rewriting to Coq. However, there are many research problems on this way. In this paper we give a coherent view of rewrit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::95d6cc5c58059d384ce08e944522b81d
https://doi.org/10.1007/978-3-540-73147-4_6
https://doi.org/10.1007/978-3-540-73147-4_6
Publikováno v:
Electronic Notes in Theoretical Computer Science. (5):113-127
Many information-flow type systems have been developed that allow to control the non-interference of information between the levels of classification in the Bell-LaPadula model. We present here a translation of typing information collected for byteco
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::037403e23786c8951e12e7481247184c