|
Mathematical Knowledge Management 2012 |
|
|
|
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar |
|
|
1 | (16) |
|
|
|
|
|
|
|
Proof, Message and Certificate |
|
|
17 | (15) |
|
|
|
Challenges and Experiences in Managing Large-Scale Proofs |
|
|
32 | (17) |
|
|
|
|
|
|
|
|
|
Semantic Alliance: A Framework for Semantic Allies |
|
|
49 | (16) |
|
|
|
|
|
|
|
|
|
Extending MKM Formats at the Statement Level |
|
|
65 | (16) |
|
|
|
|
|
|
|
A Streaming Digital Ink Framework for Multi-party Collaboration |
|
|
81 | (15) |
|
|
|
|
|
|
|
Cost-Effective Integration of MKM Semantic Services into Editing Environments |
|
|
96 | (15) |
|
|
|
Understanding the Learners' Actions when Using Mathematics Learning Tools |
|
|
111 | (16) |
|
|
|
|
|
|
|
|
|
|
|
Towards Understanding Triangle Construction Problems |
|
|
127 | (16) |
|
|
|
|
|
A Query Language for Formal Mathematical Libraries |
|
|
143 | (16) |
|
|
|
Abramowitz and Stegun - A Resource for Mathematical Document Analysis |
|
|
159 | (10) |
|
|
|
Point-and-Write - Documenting Formal Mathematics by Reference |
|
|
169 | (17) |
|
|
|
|
|
|
|
|
|
186 | (16) |
|
|
|
|
|
|
|
|
|
|
Theory Presentation Combinators |
|
|
202 | (14) |
|
|
|
|
|
Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging |
|
|
216 | (15) |
|
|
|
|
|
|
|
Towards the Formal Specification and Verification of Maple Programs |
|
|
231 | (17) |
|
|
|
|
|
Formalizing Frankl's Conjecture: FC-Families |
|
|
248 | (16) |
|
|
|
|
|
|
|
CDCL-Based Abstract State Transition System for Coherent Logic |
|
|
264 | (16) |
|
|
|
|
|
Speeding Up Cylindrical Algebraic Decomposition by Grobner Bases |
|
|
280 | (15) |
|
|
|
|
|
|
|
Artificial Intelligence and Symbolic Computation 2012 |
|
|
|
A System for Axiomatic Programming |
|
|
295 | (15) |
|
|
|
Reasoning on Schemata of Formulae |
|
|
310 | (16) |
|
|
|
|
|
Management of Change in Declarative Languages |
|
|
326 | (16) |
|
|
|
|
|
MathWebSearch 0.5: Scaling an Open Formula Search Engine |
|
|
342 | (16) |
|
|
|
|
|
Corneliu-Claudiu Prodescu |
|
|
Real Algebraic Strategies for MetiTarski Proofs |
|
|
358 | (13) |
|
|
|
|
|
|
|
A Combinator Language for Theorem Discovery |
|
|
371 | (15) |
|
|
|
|
|
Digital Mathematics Libraries 2012 |
|
|
|
DynGenPar - A Dynamic Generalized Parser for Common Mathematical Language |
|
|
386 | (16) |
|
|
|
|
|
|
|
402 | (15) |
|
|
|
|
|
Systems and Projects 2012 |
|
|
|
A Web Interface for Matita |
|
|
417 | (5) |
|
|
|
|
|
MaxTract: Converting PDF to LaTEX, MathML and Text |
|
|
422 | (5) |
|
|
|
|
|
|
|
New Developments in Parsing Mizar |
|
|
427 | (5) |
|
|
|
|
|
Open Geometry Textbook: A Case Study of Knowledge Acquisition via Collective Intelligence (Project Description) |
|
|
432 | (6) |
|
|
|
|
|
|
|
|
|
Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP) |
|
|
438 | (5) |
|
|
|
On Formal Specification of Maple Programs |
|
|
443 | (5) |
|
|
|
|
|
The Planetary Project: Towards eMath 3.0 |
|
|
448 | (5) |
|
|
|
Tentative Experiments with Ellipsis in Mizar |
|
|
453 | (5) |
|
|
|
Reimplementing the Mathematics Subject Classification (MSC) as a Linked Open Dataset |
|
|
458 | (5) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The Distributed Ontology Language (DOL): Ontology Integration and Interoperability Applied to Mathematical Formalization |
|
|
463 | (5) |
|
|
|
|
|
|
|
|
|
Isabelle/jEdit - A Prover IDE within the PIDE Framework |
|
|
468 | (5) |
|
|
| Author Index |
|
473 | |
Lisainfo e-raamatute kohta