| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban |
Large Formal Wikis: Issues and Solutions.  |
Calculemus/MKM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexey Solovyev, Thomas C. Hales |
Efficient Formal Verification of Bounds of Linear Programs. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | James H. Davenport, William M. Farmer, Josef Urban, Florian Rabe 0001 (eds.) |
Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jónathan Heras, Vico Pascual, Julio Rubio 0001 |
A System for Computing and Reasoning in Algebraic Topology. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Feryal Fulya Horozal, Alin Iacob, Constantin Jucovschi, Michael Kohlhase, Florian Rabe 0001 |
Combining Source, Content, Presentation, Narration, and Relational Representation. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | José Borbinha, Thierry Bouche, Aleksander Nowinski, Petr Sojka |
Project EuDML - A First Year Demonstration. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesse Alama |
mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Tetsuo Ida |
Proof Assistant Decision Procedures for Formalizing Origami. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban |
Licensing the Mizar Mathematical Library. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Francisco Botana |
A Symbolic Companion for Interactive Geometric Systems. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Lange 0002 |
Krextor - An Extensible Framework for Contributing Content Math to the Web of Data. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jozef Misutka, Leo Galambos |
System Description: EgoMath2 As a Tool for Mathematical Searching on Wikipedia.org. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Robbert Krebbers, Bas Spitters |
Computer Certified Efficient Exact Reals in Coq. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Distler, Muhammad Shah, Volker Sorge |
Enumeration of AG-Groupoids. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Vladimir Komendantsky, Alexander Konovalov 0001, Steve Linton |
View of Computer Algebra Data from Coq. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Mihai Codescu, Feryal Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe 0001 |
Project Abstract: Logic Atlas and Integrator (LATIN). |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Serge Autexier, Catalin David, Dominik Dietrich, Michael Kohlhase, Vyacheslav Zholudev |
Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Petr Sojka, Martin Líska |
Indexing and Searching Mathematics in Digital Libraries - Architecture, Design and Scalability Issues. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau |
Incidence Simplicial Matrices Formalized in Coq/SSReflect. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Manfred Kerber, Colin Rowat, Wolfgang Windsteiger |
Using Theorema in the Formalization of Theoretical Economics. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriel Dos Reis, David C. J. Matthews, Yue Li |
Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Deyan Ginev, Heinrich Stamerjohanns, Bruce R. Miller, Michael Kohlhase |
The LaTeXML Daemon: Editable Math on the Collaborative Web. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Bastiaan Heeren, Johan Jeuring |
Interleaving Strategies. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Robbert Krebbers, Freek Wiedijk |
A Formalization of the C99 Standard in HOL, Isabelle and Coq. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Rabe 0001, Michael Kohlhase, Claudio Sacerdoti Coen |
A Foundational View on Integration Problems. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette, William M. Farmer, Russell O'Connor |
MathScheme: Project Description. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes |
Learning2Reason. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Iain Whiteside, David Aspinall 0001, Lucas Dixon, Gudmund Grov |
Towards Formal Proof Script Refactoring. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin, Silvio Valentini |
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Makarius Wenzel |
Isabelle as Document-Oriented Proof Assistant. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Marcos Cramer, Peter Koepke, Bernhard Schröder |
Parsing and Disambiguation of Symbolic Mathematics in the Naproche System. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Cristian S. Calude, Christine Müller |
Formal Proof: Reconciling Correctness and Understanding. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Horn, Dan Roozemond |
OpenMath in SCIEnce: SCSCP and POPCORN. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | David Ruddy |
Assembling the Digital Mathematics Library. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Kohlhase, Michael Kohlhase |
Compensating the Computational Bias of Spreadsheets with MKM Techniques. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Gonzalo A. Aranda-Corral, Joaquín Borrego-Díaz, María Magdalena Fernández-Lebrón |
Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
Conservative retraction, Independence Rule, boolean derivatives |
| 1 | Christoph Lange 0002, Michael Kohlhase |
A Mathematical Approach to Ontology Authoring and Documentation. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | George Goguadze |
Representation for Interactive Exercises. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Russell J. Bradford, James H. Davenport, Christopher J. Sangwin |
A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jónathan Heras, Vico Pascual, Julio Rubio 0001 |
Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Calmet |
Abstraction-Based Information Technology: A Framework for Open Mechanized Reasoning. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
mechanized reasoning, agent, abstraction, computational modeling, knowledge |
| 1 | Ramana Chakradhar Jandhyala, Mukkai S. Krishnamoorthy, George Nagy, Raghav K. Padmanabhan, Sharad C. Seth, William Silversmith |
From Tessellations to Table Interpretation. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
rectangular tilings, X-Y trees, table grammars, Wang notation, tables, document understanding |
| 1 | Ekaterina Shemyakova |
Invariant Properties of Third-Order Non-hyperbolic Linear Partial Differential Operators. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Francisco-Jesús Martín-Mateos, Julio Rubio 0001, José-Luis Ruiz-Reina |
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Lionel Elie Mamane, Herman Geuvers, James McKinna |
A Logically Saturated Extension of lambdaµµ. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick D. F. Ion |
Some Traditional Mathematical Knowledge Management. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Kohlhase, Michael Kohlhase |
Spreadsheet Interaction with Frames: Exploring a Mathematical Practice. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | James H. Davenport, Michael Kohlhase |
Unifying Math Ontologies: A Tale of Two Standards. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette, William M. Farmer |
A Review of Mathematical Knowledge Management. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan P. Sexton, Volker Sorge, Stephen M. Watt |
Reasoning with Generic Cases in the Arithmetic of Abstract Matrices. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Grant Olney Passmore, Paul B. Jackson |
Combined Decision Techniques for the Existential Theory of the Reals. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Marko Panic |
Math Handwriting Recognition in Windows 7 and Its Benefits. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleks Kissinger |
Exploring a Quantum Theory with Graph Rewriting and Computer Algebra. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Lamar, Fairouz Kamareddine, J. B. Wells |
MathLang Translation to Isabelle Syntax. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Josef B. Baker, Alan P. Sexton, Volker Sorge |
A Linear Grammar Approach to Mathematical Formula Recognition from PDF. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Bastiaan Heeren, Johan Jeuring |
Canonical Forms in Interactive Exercise Assistants. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, Stephen M. Watt (eds.) |
Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | John P. Fitch |
CAMAL 40 Years on - Is Small Still Beautiful?. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Paul Tarau |
A Groupoid of Isomorphic Data Transformations. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
computational mathematics in Haskell, data type transformations, ranking/unranking, Gödel numberings, higher order combinators, hylomorphisms |
| 1 | Dorothea Blostein |
Math-Literate Computers. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jana Giceva, Christoph Lange 0002, Florian Rabe 0001 |
Integrating Web Services into Active Mathematical Documents. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Aslam Muhammad 0001, Ana María Martínez Enríquez, Gonzalo Escalada-Imaz |
Collaborative Assistant to Handle MathML Expressions. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
Knowledge based systems, awareness, collaborative writing, MathML |
| 1 | Rob Arthan |
Computational Logic and Continuous Mathematics, Pure and Applied. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Sidi Ould Biha |
Finite Groups Representation Theory with Coq. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
Maschke’s theorem, SSReflect, linear algebra, Coq, Representation theory |
| 1 | Stephen M. Watt |
Algorithms for the Functional Decomposition of Laurent Polynomials. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Oleg Golubitsky, Stephen M. Watt |
Confidence Measures in Recognizing Handwritten Mathematical Symbols. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph B. Collins |
OpenMath Content Dictionaries for SI Quantities and Units. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Claudio Sacerdoti Coen, Enrico Tassi |
Natural Deduction Environment for Matita. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond |
Combining Coq and Gappa for Certifying Floating-Point Programs. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Davood G. Gozli, Marco Pollanen, Michael G. Reynolds |
The Characteristics of Writing Environments for Mathematics: Behavioral Consequences and Implications for Software Design and Usability. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Albert D. Rich, David J. Jeffrey |
A Knowledge Repository for Indefinite Integration Based on Transformation Rules. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Georges Gonthier |
Software Engineering for Mathematics. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Coquand, Arnaud Spiwack |
Towards Constructive Homological Algebra in Type Theory. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Corbineau, Cezary Kaliszyk |
Cooperative Repositories for Formal Proofs. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette, William M. Farmer, Volker Sorge |
A Rational Reconstruction of a System for Experimental Mathematics. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Serge Autexier, Armin Fiedler, Thomas Neumann 0006, Marc Wagner 0001 |
Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | William M. Farmer |
Biform Theories in Chiron. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel, J. B. Wells |
Narrative Structure of Mathematical Texts. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Klaus Grue |
The Layers of Logiweb. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Claudio Sacerdoti Coen, Stefano Zacchiroli |
Spurious Disambiguation Error Detection. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Ewa Borak, Anna Zalewska |
Mizar Course in Logic and Set Theory. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Murray-Rust |
Mathematics and Scientific Markup. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger (eds.) |
Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Neil J. A. Sloane |
The On-Line Encyclopedia of Integer Sequences. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Immanuel Normann, Michael Kohlhase |
Extended Formula Normalization for epsilon -Retrieval and Sharing of Mathematical Knowledge. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Grabowski, Christoph Schwarzweller |
Revisions as an Essential Tool to Maintain Mathematical Repositories. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Abdou Youssef |
Methods of Relevance Ranking and Hit-content Generation in Math Search. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Feryal Fulya Horozal, Chad E. Brown |
Formal Representation of Mathematics in a Dependently Typed Set Theory. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilbert Lee, Piotr Rudnicki |
Alternative Aggregates in Mizar. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Amine Chaieb, Makarius Wenzel |
Context Aware Calculation and Deduction. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Songxin Liang, David J. Jeffrey |
Rule-Based Simplification in Vector-Product Spaces. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Colton, Daniel Wagner 0002 |
Using Formal Concept Analysis in Mathematical Discovery. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Enrico Tassi |
Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | James H. Davenport |
What Might "Understand a Function" Mean? |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Predrag Janicic, Alan Bundy |
Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Freek Wiedijk |
Certified Computer Algebra on Top of an Interactive Theorem Prover. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Agnieszka Rowinska-Schwarzweller, Christoph Schwarzweller |
Towards Mathematical Knowledge Management for Electrical Engineering. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Miner, Rajesh Munavalli |
An Approach to Mathematical Search Through Query Formulation and Data Normalization. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Miguel A. Abánades, Jesús Escribano, Francisco Botana |
First Steps on Using OpenMath to Add Proving Capabilities to Standard Dynamic Geometry Systems. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Kohlhase, Michael Kohlhase |
Re examining the MKM Value Proposition: From Math Web Search to Math Web Re Search. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license