| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Andrea Asperti |
Proof, Message and Certificate.  |
AISC/MKM/Calculemus  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Muhammad Taimoor Khan 0001, Wolfgang Schreiner |
Towards the Formal Specification and Verification of Maple Programs. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Kevin Kofler, Arnold Neumaier |
DynGenPar - A Dynamic Generalized Parser for Common Mathematical Language. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Kohlhase, Bogdan Matican, Corneliu-Claudiu Prodescu |
MathWebSearch 0.5: Scaling an Open Formula Search Engine. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Carst Tankink, Christoph Lange 0002, Josef Urban |
Point-and-Write - Documenting Formal Mathematics by Reference. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette, Russell O'Connor |
Theory Presentation Combinators. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Grant Olney Passmore, Lawrence C. Paulson, Leonardo Mendonça de Moura |
Real Algebraic Strategies for MetiTarski Proofs. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Lange 0002, Patrick Ion, Anastasia Dimou, Charalampos Bratsas, Joseph Corneli, Wolfram Sperber, Michael Kohlhase, Ioannis Antoniou |
Reimplementing the Mathematics Subject Classification (MSC) as a Linked Open Dataset. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriel Dos Reis |
A System for Axiomatic Programming. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan P. Sexton |
Abramowitz and Stegun - A Resource for Mathematical Document Analysis. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Paul Libbrecht, Sandra Rebholz, Daniel Herding, Wolfgang Müller 0004, Felix Tscheulin |
Understanding the Learners' Actions when Using Mathematics Learning Tools. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Czeslaw Bylinski, Jesse Alama |
New Developments in Parsing Mizar. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jónathan Heras, María Poza, Julio Rubio 0001 |
Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Mihnea Iancu, Florian Rabe 0001 |
Management of Change in Declarative Languages. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Artur Kornilowicz |
Tentative Experiments with Ellipsis in Mizar. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Xiaoyu Chen 0001, Wei Li 0022, Jie Luo 0004, Dongming Wang 0001 |
Open Geometry Textbook: A Case Study of Knowledge Acquisition via Collective Intelligence - (Project Description). |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Muhammad Taimoor Khan 0001, Wolfgang Schreiner |
On Formal Specification of Maple Programs. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Timothy Bourke, Matthias Daum 0001, Gerwin Klein, Rafal Kolanski |
Challenges and Experiences in Managing Large-Scale Proofs. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Vadim Mazalov, Stephen M. Watt |
Writing on Clouds. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Constantin Jucovschi |
Cost-Effective Integration of MKM Semantic Services into Editing Environments. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesse Alama, Lionel Mamane, Josef Urban |
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Rui Hu, Vadim Mazalov, Stephen M. Watt |
A Streaming Digital Ink Framework for Multi-party Collaboration. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Iain Whiteside, David Aspinall 0001, Gudmund Grov |
An Essence of SSReflect. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Josef B. Baker, Alan P. Sexton, Volker Sorge |
MaxTract: Converting PDF to $\mbox\LaTeX$ , MathML and Text. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Makarius Wenzel |
Isabelle/jEdit - A Prover IDE within the PIDE Framework. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Rabe 0001 |
A Query Language for Formal Mathematical Libraries. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | David J. Wilson, Russell J. Bradford, James H. Davenport |
Speeding Up Cylindrical Algebraic Decomposition by Gröbner Bases. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Phil Scott, Jacques D. Fleuriot |
A Combinator Language for Theorem Discovery. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Lange 0002, Oliver Kutz, Till Mossakowski, Michael Grüninger |
The Distributed Ontology Language (DOL): Ontology Integration and Interoperability Applied to Mathematical Formalization. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Vesna Marinkovic, Predrag Janicic |
Towards Understanding Triangle Construction Problems. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Wilmer Ricciotti |
A Web Interface for Matita. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, Volker Sorge (eds.) |
Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Kohlhase |
The Planetary Project: Towards eMath3.0. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Nicolas Peltier |
Reasoning on Schemata of Formulæ. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Hetzl |
Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP). |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Mladen Nikolic, Predrag Janicic |
CDCL-Based Abstract State Transition System for Coherent Logic. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Feryal Fulya Horozal, Michael Kohlhase, Florian Rabe 0001 |
Extending MKM Formats at the Statement Level. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Filip Maric, Miodrag V. Zivkovic, Bojan Vuckovic |
Formalizing Frankl's Conjecture: FC-Families. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Catalin David, Constantin Jucovschi, Andrea Kohlhase, Michael Kohlhase |
Semantic Alliance: A Framework for Semantic Allies. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Bastiaan Heeren, Johan Jeuring |
Adapting Mathematical Domain Reasoners. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Manfred Kerber |
Proofs, Proofs, Proofs, and Proofs. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Maksym Bortin, Christoph Lüth |
Structured Formal Development with Quotient Types in Isabelle/HOL. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | César Domínguez 0001, Julio Rubio 0001 |
Computing in Coq with Infinite Algebraic Data Structures. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers |
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jónathan Heras, Vico Pascual, Ana Romero 0001, Julio Rubio 0001 |
Integrating Multiple Sources to Answer Questions in Algebraic Topology. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Mikhail K. Kolev |
A Mathematical Model of the Competition between Acquired Immunity and Virus. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Kohlhase, Michael Kohlhase, Christoph Lange 0002 |
Dimensions of Formality: A Case Study for MKM in Software Engineering. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Paul Libbrecht |
Notations Around the World: Census and Exploitation. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | David J. Jeffrey, Albert D. Rich |
Reducing Expression Size Using Rule-Based Integration. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Bruno Salvy |
The Dynamic Dictionary of Mathematical Functions. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette |
Mechanized Mathematics. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Agnieszka Rowinska-Schwarzweller, Christoph Schwarzweller |
On Building a Knowledge Base for Stability Theory. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | James H. Davenport |
The Challenges of Multivalued "Functions". |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Yongbin Li |
Some Notes upon "When Does Equal Sat(T)?". |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Josef Urban, Geoff Sutcliffe |
Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk |
Proviola: A Tool for Proof Re-animation. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Franck Butelle, Florent Hivert, Micaela Mayero, Frédéric Toumazet |
Formal Proof of SCHUR Conjugate Function. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Doron Zeilberger |
Against Rigor. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Vincent Loddo, Luca Saiu |
How to Correctly Prune Tropical Trees. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Constantin Jucovschi, Michael Kohlhase |
sTeXIIS: An Integrated Development Environment for sTeX Collections. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Nicolas Peltier |
Instantiation of SMT Problems Modulo Integers. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Salvador Lucas |
From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Enrico Tassi |
Smart Matching. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andriy Kovalchuk, Vyacheslav Levitsky, Igor Samolyuk, Valentyn Yanchuk |
The Formulator MathML Editor Project: User-Friendly Authoring of Content Markup Documents. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Kohlhase, Florian Rabe 0001, Vyacheslav Zholudev |
Towards MKM in the Large: Modular Representation and Scalable Software Architecture. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph B. Collins |
An OpenMath Content Dictionary for Tensor Concepts. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander V. Lyaletski, Konstantin Verchinine |
Evidence Algorithm and System for Automated Deduction: A Retrospective View. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Grabowski, Christoph Schwarzweller |
On Duplication in Mathematical Repositories. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Xiaoyu Chen |
Electronic Geometry Textbook: A Geometric Textbook Knowledge Management System. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Paul Tarau |
A Unified Formal Description of Arithmetic and Set Theoretical Data Types. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Calmet, John A. Campbell |
A Revisited Perspective on Symbolic Mathematical Computing and Artificial Intelligence. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ioana Pasca |
Formally Verified Conditions for Regularity of Interval Matrices. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette, Alan P. Sexton, Volker Sorge, Stephen M. Watt |
Symbolic Domain Decomposition. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Cyril Cohen, Assia Mahboubi |
A Formal Quantifier Elimination for Algebraically Closed Fields. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Philip Feinsilver, René Schott |
On Krawtchouk Transforms. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Claudio Sacerdoti Coen |
Some Considerations on the Usability of Interactive Provers. |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, Alan P. Sexton (eds.) |
Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings |
AISC/MKM/Calculemus |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer, Makarius Wenzel |
Logic-Free Reasoning in Isabelle/Isar. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph B. Collins |
A Mathematical Type for Physical Variables. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Manfred Kerber |
Normalization Issues in Mathematical Representations. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Lucas Dixon, Ross Duncan |
Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
categorical logic, graphical calculi, quantum computing, graph rewriting, interactive theorem proving |
| 1 | James H. Davenport |
AISC Meets Natural Typography. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Bruce R. Miller, Abdou Youssef |
Augmenting Presentation MathML for Search. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Amine Chaieb |
Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Franky Backeljauw, Stefan Becuwe, Annie A. M. Cuyt |
Validated Evaluation of Special Mathematical Functions. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Oleg Lobachev, Rita Loogen |
Towards an Implementation of a Computer Algebra System in a Functional Language. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
language and system design, computer algebra, software technology |
| 1 | Thierry Bouche |
Digital Mathematics Libraries: The Good, the Bad, the Ugly. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | John William Charnley, Simon Colton |
A Global Workspace Framework for Combining Reasoning Systems. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Behzad Akbarpour, Lawrence C. Paulson |
MetiTarski: An Automatic Prover for the Elementary Functions. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Hetzl, Alexander Leitsch, Daniel Weller 0001, Bruno Woltzenlogel Paleo |
Herbrand Sequent Extraction. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Steve Linton |
Symmetry and Search - A Survey. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Bastiaan Heeren, Johan Jeuring, Arthur van Leeuwen, Alex Gerdes |
Specifying Strategies for Exercises. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Kohlhase, Christine Müller, Florian Rabe 0001 |
Notations for Living Mathematical Documents. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich, Anatoly V. Anisimov |
On Correctness of Mathematical Texts from a Logical and Practical Point of View. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä |
Strategies for Solving SAT in Grids by Randomized Search. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | John Howse, Gem Stapleton |
Visual Mathematics: Diagrammatic Formalization and Proof. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Teguh Bharata Adji, Baharum Baharudin, Norshuhani Zamin |
Applying Link Grammar Formalism in the Development of English-Indonesian Machine Translation System. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
Annotated Disjunct, Link Grammar, Parsing Algorithm, Natural Language Processing |
| 1 | Sebastian Freundt, Peter Horn, Alexander Konovalov 0001, Steve Linton, Dan Roozemond |
Symbolic Computation Software Composability. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Eugenio Roanes-Lozano, Luis M. Laita, Eugenio Roanes-Macías |
A Groebner Bases Based Many-Valued Modal Logic Implementation in Maple. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
Logic and Symbolic Computing, Rule Based Expert Systems, Groebner Bases |
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license