Search

Your search keyword '"Mamane, L.E."' showing total 14 results
Start Over Author "Mamane, L.E."
14 results on '"Mamane, L.E."'

1. A Logically Saturated Extension of λμ¯ μ

Author

Mamane, L.E., Geuvers, J.H., McKinna, J.H., Carette, J., Dixon, L., Coen, Claudio Sacerdoti, Watt, Stephen M., Carette, J., Dixon, L., Coen, Claudio Sacerdoti, and Watt, Stephen M.

Subjects
Data Science
Abstract

Item does not contain fulltext Proceedings of 8th International Conference, 16th Symposium, Calculemus 2009 CICM '09 on Intelligent Computer Mathematics, 06 juli 2009

Published
2009

2. A logically saturated extension of $\bar{\lambda} \mu \tilde{\mu}$

Author

Mamane, L.E., Geuvers, J.H., McKinna, J., Carette, J., Dixon, L., Sacerdoti Coen, C., Watt, S.M., and Formal System Analysis

Subjects
Mathematics education
Abstract

This paper presents a proof language based on the work of Sacerdoti Coen [1,2], Kirchner [3] and Autexier [4] on ¯¿µ˜µ, a calculus introduced by Curien and Herbelin [5,6]. Just as ¯¿µ˜µ preserves several proof structures that are identified by the ¿-calculus, the proof language presented here aims to preserve as much proof structure as reasonable; we call that property being logically saturated. This leads to several advantages when the language is used as a generic exchange language for proofs, as well as for other uses. We equip the calculus with a simple rendering in pseudo-natural language that aims to give people tools to read, understand and exchange terms of the language. We show how this rendering can, at the cost of some more complexity, be made to produce text that is more natural and idiomatic, or in the style of a declarative proof language like Isar or Mizar.

Published
2009
Full Text
View/download PDF

3. Interactive mathematical documents : creation and presentation

Author

Mamane, L.E., Geuvers, J.H., McKinna, J.H., and Radboud University Nijmegen

Subjects
Data Science, IPA dissertation series
Abstract

Contains fulltext : 122866.pdf (Publisher’s version ) (Open Access) Radboud Universiteit Nijmegen, 23 september 2013 Promotor : Geuvers, J.H. Co-promotor : McKinna, J.H. 199 p.

Published
2013

4. Licensing the Mizar mathematical library

Author

Alama, J.A., Kohlhase, M., Mamane, L.E., Naumowicz, A., Rudnicki, P., Urban, J., Davenport, J., Farmer, W., Rabe, F., Davenport, J., Farmer, W., Urban, J., and Rabe, F.

Subjects
Scheme (programming language), Cloning (programming), Programming language, Computer science, Data Science, Proof assistant, Lecture Notes in Computer Science, Mizar system, computer.software_genre, computer, computer.programming_language
Abstract

We present several steps towards large formal mathematical wikis. The Coq proof assistant together with the CoRN repository are added to the pool of systems handled by the general wiki system described in \cite{DBLP:conf/aisc/UrbanARG10}. A smart re-verification scheme for the large formal libraries in the wiki is suggested for Mizar/MML and Coq/CoRN, based on recently developed precise tracking of mathematical dependencies. We propose to use features of state-of-the-art filesystems to allow real-time cloning and sandboxing of the entire libraries, allowing also to extend the wiki to a true multi-user collaborative area. A number of related issues are discussed.

Published
2011
Full Text
View/download PDF

5. A Logically Saturated Extension of ¯λμ˜μ

Author

Mamane, L.E., Geuvers, J.H., and McKinna, J.H.

Subjects
Technical Report, Computer Science::Logic in Computer Science, Data Science, Computer Science::Data Structures and Algorithms
Abstract

Contains fulltext : 76119.pdf (author's version ) (Open Access) A Logically Saturated Extension of [`(l)]m[(m)\tilde]λˉμμ˜ 26 p.

Published
2009

6. Surreal Numbers in Coq

Author

Mamane, L.E., Filliâtre, Jean-Chris, Paulin-Mohring, Christine, Werner, Benjamin, Filliâtre, Jean-Chris, Paulin-Mohring, Christine, and Werner, Benjamin

Subjects
Lecture Notes in Computer Science, Foundations
Abstract

Item does not contain fulltext

Published
2006

7. Interactive mathematical documents : creation and presentation

Author

Geuvers, J.H., McKinna, J.H., Mamane, L.E., Geuvers, J.H., McKinna, J.H., and Mamane, L.E.

Abstract

Radboud Universiteit Nijmegen, 23 september 2013, Promotor : Geuvers, J.H. Co-promotor : McKinna, J.H., Contains fulltext : 122866.pdf (Publisher’s version ) (Open Access)

Published
2013

8. Large Formal Wikis: Issues and Solutions

Author

Davenport, J., Farmer, W., Urban, J., Rabe, F., Alama, J.A., Brink, K.J., Mamane, L.E., Davenport, J., Farmer, W., Urban, J., Rabe, F., Alama, J.A., Brink, K.J., and Mamane, L.E.

Abstract

Contains fulltext : 91990.pdf (publisher's version ) (Closed access)

Published
2011

9. Licensing the Mizar mathematical library

Author

Davenport, J., Farmer, W., Urban, J., Rabe, F., Alama, J.A., Kohlhase, M., Mamane, L.E., Naumowicz, A., Rudnicki, P., Davenport, J., Farmer, W., Urban, J., Rabe, F., Alama, J.A., Kohlhase, M., Mamane, L.E., Naumowicz, A., and Rudnicki, P.

Abstract

Contains fulltext : 92003.pdf (publisher's version ) (Closed access)

Published
2011

10. A Logically Saturated Extension of λμ¯ μ

Author

Carette, J., Dixon, L., Coen, Claudio Sacerdoti, Watt, Stephen M., Mamane, L.E., Geuvers, J.H., McKinna, J.H., Carette, J., Dixon, L., Coen, Claudio Sacerdoti, Watt, Stephen M., Mamane, L.E., Geuvers, J.H., and McKinna, J.H.

Abstract

Proceedings of 8th International Conference, 16th Symposium, Calculemus 2009 CICM '09 on Intelligent Computer Mathematics, 6 juli 2009, Item does not contain fulltext

Published
2009

13. Surreal Numbers in Coq

Author

Filliâtre, Jean-Chris, Paulin-Mohring, Christine, Werner, Benjamin, Mamane, L.E., Filliâtre, Jean-Chris, Paulin-Mohring, Christine, Werner, Benjamin, and Mamane, L.E.

Abstract

Item does not contain fulltext

Published
2006

Catalog

Books, media, physical & digital resources
See catalog results