Mathematical discourse : language, symbolism and visual images / / Kay L. O'Halloran

• Record Nr.: UNINA9910456788603321
• Autore: O'Halloran Kay L.
• Pubbl/distr/stampa: London, [England] ; ; New York, New York : , : Continuum, , 2005; ©2005
• ISBN: 1-4411-7737-X
• Descrizione fisica: 1 online resource (239 p.)
• Disciplina: 510.1/4
• Soggetti: Mathematics - Language; Mathematics; Visualization; Electronic books.
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Description based upon print version of record.
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Cover; Contents; Acknowledgements; Copyright Permission Acknowledgements; 1 Mathematics as a Multisemiotic Discourse; 1.1 The Creation of Order; 1.2 Halliday''s Social Semiotic Approach; 1.3 Mathematics as Multisemiotic; 1.4 Implications of a Multisemiotic View; 1.5 Tracing the Semiotics of Mathematics; 1.6 Systemic Functional Research in Multimodality; 2 Evolution of the Semiotics of Mathematics; 2.1 Historical Development of Mathematical Discourse; 2.2 Early Printed Mathematics Books; 2.3 Mathematics in the Early Renaissance; 2.4 Beginnings of Modern Mathematics: Descartes and Newton; 2.5 Descartes'' Philosophy and Semiotic Representations2.6 A New World Order; 3 Systemic Functional Linguistics (SFL) and Mathematical Language; 3.1 The Systemic Functional Model of Language; 3.2 Interpersonal Meaning in Mathematics; 3.3 Mathematics and the Language of Experience; 3.4 The Construction of Logical Meaning; 3.5 The Textual Organization of Language; 3.6 Grammatical Metaphor and Mathematical Language; 3.7 Language, Context and Ideology; 4 The Grammar of Mathematical Symbolism; 4.1 Mathematical Symbolism; 4.2 Language-Based Approach to Mathematical Symbolism; 4.3 SF Framework for Mathematical Symbolism4.4 Contraction and ; Expansion of Experiential Meaning; 4.5 Contraction of Interpersonal Meaning; 4.6 A Resource for Logical Reasoning; 4.7 Specification of Textual Meaning; 4.8 Discourse, Grammar and Display; 4.9 Concluding Comments; 5 The Grammar of Mathematical Visual Images; 5.1 The Role of Visualization in Mathematics; 5.2 SF Framework for Mathematical Visual Images; 5.3 Interpersonally Orientating the Viewer; 5.4 Visual Construction of Experiential Meaning; 5.5 Reasoning through Mathematical Visual Images; 5.6 Compositional Meaning and Conventionalized Styles of Organization5.7 Computer Graphics and the New Image of Mathematics; 6 Intersemiosis: Meaning Across Language, Visual Images and Symbolism; 6.1 The Semantic Circuit in Mathematics; 6.2 Intersemiosis: Mechanisms, Systems and Semantics; 6.3 Analysing Intersemiosis in Mathematical Texts; 6.4 Intersemiotic Re-Contexualization in Newton''s Writings; 6.5 Semiotic Metaphor and Metaphorical Expansions of Meaning; 6.6 Reconceptualizing Grammatical Metaphor; 7 Mathematical Constructions of Reality; 7.1 Multisemiotic Analysis of a Contemporary Mathematics Problem7.2 Educational Implications of a Multisemiotic Approach to Mathematics; 7.3 Pedagogical Discourse in Mathematics Classrooms; 7.4 The Nature and Use of Mathematical Constructions; References; Index; A; B; C; D; E; F; G; H; I; K; L; M; N; O; P; R; S; T; V; W
• Sommario/riassunto: This book examines mathematical discourse from the perspective of Michael Halliday''s social semiotic theory. In this approach, mathematics is conceptualized as a multisemiotic discourse involving language, visual images and symbolism. The book discusses the evolution of the semiotics of mathematical discourse, and then, proceeds to examine the grammar of mathematical symbolism, the grammar of mathematical visual images, intersemiosis between language, visual images and symbolism and the subsequent ways in which mathematics orders reality. The focus of this investigation is written mathema

Automated Reasoning : Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings / / edited by Ulrich Furbach, Natarajan Shankar

• Record Nr.: UNINA9910767562503321
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006
• ISBN: 3-540-37188-5
• Edizione: [1st ed. 2006.]
• Descrizione fisica: 1 online resource (XVI, 688 p.)
• Collana: Lecture Notes in Artificial Intelligence, , 2945-9141 ; ; 4130
• Altri autori (Persone): FurbachUlrich; ShankarN (Natarajan)
• Disciplina: 006.3
• Soggetti: Artificial intelligence; Machine theory; Computer science; Software engineering; Artificial Intelligence; Formal Languages and Automata Theory; Computer Science Logic and Foundations of Programming; Software Engineering
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Invited Talks -- Mathematical Theory Exploration -- Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation -- Representing and Reasoning with Operational Semantics -- Session 1. Proofs -- Flyspeck I: Tame Graphs -- Automatic Construction and Verification of Isotopy Invariants -- Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms -- Using the TPTP Language for Writing Derivations and Finite Interpretations -- Session 2. Search -- Stratified Context Unification Is NP-Complete -- A Logical Characterization of Forward and Backward Chaining in the Inverse Method -- Connection Tableaux with Lazy Paramodulation -- Blocking and Other Enhancements for Bottom-Up Model Generation Methods -- Session 3. System Description 1 -- The MathServe System for Semantic Web ; Reasoning Services -- System Description: GCLCprover + GeoThms -- A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms -- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation -- Session 4. Higher-Order Logic -- Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics -- Towards Self-verification of HOL Light -- An Interpretation of Isabelle/HOL in HOL Light -- Combining Type Theory and Untyped Set Theory -- Session 5. Proof Theory -- Cut-Simulation in Impredicative Logics -- Interpolation in Local Theory Extensions -- Canonical Gentzen-Type Calculi with (n,k)-ary Quantifiers -- Dynamic Logic with Non-rigid Functions -- Session 6. System Description 2 -- AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework -- CEL — A Polynomial-Time Reasoner for Life Science Ontologies -- FaCT++ Description Logic Reasoner: System Description -- Importing HOL intoIsabelle/HOL -- Session 7. Search -- Geometric Resolution: A Proof Procedure Based on Finite Model Search -- A Powerful Technique to Eliminate Isomorphism in Finite Model Search -- Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems -- Session 8. Proof Theory -- Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic -- Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach -- First-Order Logic with Dependent Types -- Session 9. Proof Checking -- Automating Proofs in Category Theory -- Formal Global Optimisation with Taylor Models -- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers -- Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials -- Session 10. Combination -- A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) -- Solving Sparse Linear Constraints -- Inferring Network Invariants Automatically -- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL -- Session 11. Decision Procedures -- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures -- Verifying Mixed Real-Integer Quantifier Elimination -- Presburger Modal Logic Is PSPACE-Complete -- Tree Automata with Equality Constraints Modulo Equational Theories -- Session 12. CASC-J3 -- CASC-J3 The 3rd IJCAR ATP System Competition -- Session 13. Rewriting -- Matrix Interpretations for Proving Termination of Term Rewriting -- Partial Recursive Functions in Higher-Order Logic -- On the Strength of Proof-Irrelevant Type Theories -- Consistency and Completeness of Rewriting in the Calculus of Constructions -- Session 14. Description Logic -- Specifying and Reasoning About DynamicAccess-Control Policies -- On Keys and Functional Dependencies as First-Class Citizens in Description Logics -- A Resolution-Based Decision Procedure for .
• Sommario/riassunto: This book constitutes the refereed proceedings of the Third International Joint Conference on Automated Reasoning, IJCAR 2006, held in Seattle, WA, USA in August 2006 as part of the 4th Federated Logic Conference, FLoC 2006. IJCAR 2006 is a merger of CADE, FroCoS, FTP, TABLEAUX, and TPHOLs. The 41 revised full research papers and 8 revised system descriptions presented together with 3 invited papers and a summary of a systems competition were carefully reviewed and selected from a total of 152 submissions. The papers address the entire spectrum of research in automated reasoning including formalization of mathematics, proof theory, proof search, description logics, interactive proof checking, higher-order logic, combination methods, satisfiability procedures, and rewriting. The papers are organized in topical sections on proofs, search, higher-order logic, ; proof theory, search, proof checking, combination, decision procedures, CASC-J3, rewriting, and description logic.