Towards Mechanized Mathematical Assistants
Editat de Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteigeren Limba Engleză Paperback – 19 iun 2007
Preț: 382.45 lei
Nou
Puncte Express: 574
Preț estimativ în valută:
67.67€ • 78.83$ • 59.09£
67.67€ • 78.83$ • 59.09£
Carte tipărită la comandă
Livrare economică 19 ianuarie-02 februarie 26
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9783540730835
ISBN-10: 3540730834
Pagini: 424
Ilustrații: XIII, 410 p.
Dimensiuni: 155 x 235 x 23 mm
Greutate: 0.64 kg
Ediția:2007
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540730834
Pagini: 424
Ilustrații: XIII, 410 p.
Dimensiuni: 155 x 235 x 23 mm
Greutate: 0.64 kg
Ediția:2007
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
Contributions to Calculemus 2007.- Executing in Common Lisp, Proving in ACL2.- A Rational Reconstruction of a System for Experimental Mathematics.- Context Aware Calculation and Deduction.- Towards Constructive Homological Algebra in Type Theory.- What Might “Understand a Function” Mean?.- Biform Theories in Chiron.- Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic.- Certified Computer Algebra on Top of an Interactive Theorem Prover.- Quantifier Elimination for Approximate Factorization of Linear Partial Differential Operators.- Rule-Based Simplification in Vector-Product Spaces.- Contributions to MKM 2007.- Mathematics and Scientific Markup.- The On-Line Encyclopedia of Integer Sequences.- First Steps on Using OpenMath to Add Proving Capabilities to Standard Dynamic Geometry Systems.- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case.- A Framework for Interactive Proof.- Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems.- Mizar Course in Logic and Set Theory.- Using Formal Concept Analysis in Mathematical Discovery.- Cooperative Repositories for Formal Proofs.- Revisions as an Essential Tool to Maintain Mathematical Repositories.- The Layers of Logiweb.- Formal Representation of Mathematics in a Dependently Typed Set Theory.- Restoring Natural Language as a Computerised Mathematics Input Method.- Narrative Structure of Mathematical Texts.- Reexamining the MKM Value Proposition: From Math Web Search to Math Web ReSearch.- Alternative Aggregates in Mizar.- An Approach to Mathematical Search Through Query Formulation and Data Normalization.- Extended Formula Normalization for ?-Retrieval and Sharing of Mathematical Knowledge.-Towards Mathematical Knowledge Management for Electrical Engineering.- Spurious Disambiguation Error Detection.- Methods of Relevance Ranking and Hit-content Generation in Math Search.