Listing 1 - 10 of 19 | << page >> |
Sort by
|
Choose an application
This book constitutes the refereed proceedings of the 9th International Conference on Rewriting Techniques and Applications, RTA-98, held in Tsukuba, Japan, in March/April 1998. The 22 revised full papers presented were carefully selected from a total of 61 submissions by the program committee with the assistance of 113 additional referees. The book covers all current aspects of rewriting including rewriting systems, term rewriting, string rewriting, theorem proving, resolution, normalization, unification, equational logics, lambda calculus, constraint solving, and functional programming.
Rewriting systems (Computer science) --- Computer programming --- Algorithms --- Computer science. --- Programming languages (Electronic computers). --- Computer logic. --- Mathematical logic. --- Artificial intelligence. --- Computer Science. --- Programming Languages, Compilers, Interpreters. --- Mathematical Logic and Formal Languages. --- Logics and Meanings of Programs. --- Artificial Intelligence (incl. Robotics). --- Mathematical Logic and Foundations. --- AI (Artificial intelligence) --- Artificial thinking --- Electronic brains --- Intellectronics --- Intelligence, Artificial --- Intelligent machines --- Machine intelligence --- Thinking, Artificial --- Bionics --- Cognitive science --- Digital computer simulation --- Electronic data processing --- Logic machines --- Machine theory --- Self-organizing systems --- Simulation methods --- Fifth generation computers --- Neural computers --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Computer science logic --- Logic, Symbolic and mathematical --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Languages, Artificial --- Informatics --- Science --- Congresses --- Electronic digital computers --- Programming --- Logic design. --- Logic, Symbolic and mathematical. --- Artificial Intelligence. --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Switching theory --- Computer programming. --- Computers --- Electronic computer programming --- Programming (Electronic computers) --- Coding theory --- Rewriting systems (Computer science) - Congresses --- Computer programming - Congresses --- Algorithms - Congresses
Choose an application
Choose an application
Part I of this book is a practical introduction to working with the Isabelle proof assistant. It teaches you how to write functional programs and inductive definitions and how to prove properties about them in Isabelle’s structured proof language. Part II is an introduction to the semantics of imperative languages with an emphasis on applications like compilers and program analysers. The distinguishing feature is that all the mathematics has been formalised in Isabelle and much of it is executable. Part I focusses on the details of proofs in Isabelle; Part II can be read even without familiarity with Isabelle’s proof language, all proofs are described in detail but informally. The book teaches the reader the art of precise logical reasoning and the practical use of a proof assistant as a surgical tool for formal proofs about computer science artefacts. In this sense it represents a formal approach to computer science, not just semantics. The Isabelle formalisation, including the proofs and accompanying slides, are freely available online, and the book is suitable for graduate students, advanced undergraduate students, and researchers in theoretical computer science and logic.
Engineering & Applied Sciences --- Computer Science --- Computer science. --- Programming languages (Electronic computers). --- Computer logic. --- Mathematical logic. --- Computer Science. --- Logics and Meanings of Programs. --- Programming Languages, Compilers, Interpreters. --- Mathematical Logic and Formal Languages. --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Computer science logic --- Logic, Symbolic and mathematical --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Electronic data processing --- Languages, Artificial --- Informatics --- Science --- Logic design. --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory
Choose an application
This textbook offers a unified and self-contained introduction to the field of term rewriting. It covers all the basic material (abstract reduction systems, termination, confluence, completion, and combination problems), but also some important and closely connected subjects: universal algebra, unification theory, Gröbner bases and Buchberger's algorithm. The main algorithms are presented both informally and as programs in the functional language Standard ML (an appendix contains a quick and easy introduction to ML). Certain crucial algorithms like unification and congruence closure are covered in more depth and Pascal programs are developed. The book contains many examples and over 170 exercises. This text is also an ideal reference book for professional researchers: results that have been spread over many conference and journal articles are collected together in a unified notation, proofs of almost all theorems are provided, and each chapter closes with a guide to the literature.
Choose an application
Choose an application
Part I of this book is a practical introduction to working with the Isabelle proof assistant. It teaches you how to write functional programs and inductive definitions and how to prove properties about them in Isabelle’s structured proof language. Part II is an introduction to the semantics of imperative languages with an emphasis on applications like compilers and program analysers. The distinguishing feature is that all the mathematics has been formalised in Isabelle and much of it is executable. Part I focusses on the details of proofs in Isabelle; Part II can be read even without familiarity with Isabelle’s proof language, all proofs are described in detail but informally. The book teaches the reader the art of precise logical reasoning and the practical use of a proof assistant as a surgical tool for formal proofs about computer science artefacts. In this sense it represents a formal approach to computer science, not just semantics. The Isabelle formalisation, including the proofs and accompanying slides, are freely available online, and the book is suitable for graduate students, advanced undergraduate students, and researchers in theoretical computer science and logic.
Mathematical logic --- Logic --- Computer science --- Programming --- computers --- ontwerpen --- programmeren (informatica) --- programmeertalen --- wiskunde --- logica --- computerkunde
Choose an application
Choose an application
This volume contains thoroughly refereed and revised full papers selected from the presentations at the first workshop held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs in Nijmegen, The Netherlands, in May 1993. As the whole ESPRIT BRA 6453, this volume is devoted to the theoretical foundations, design and applications of systems for theory development. Such systems help in designing mathematical axiomatisation, performing computer-aided logical reasoning, and managing databases of mathematical facts; they are also known as proof assistants or proof checkers.
Automatic theorem proving --- Computer programs --- Théorèmes --- Logiciels --- Congresses. --- Démonstration automatique --- Congrès --- Théorèmes --- Démonstration automatique --- Congrès --- Congresses --- Information theory. --- Software engineering. --- Computer science. --- Logic design. --- Artificial intelligence. --- Theory of Computation. --- Software Engineering/Programming and Operating Systems. --- Mathematical Logic and Formal Languages. --- Logics and Meanings of Programs. --- Artificial Intelligence. --- AI (Artificial intelligence) --- Artificial thinking --- Electronic brains --- Intellectronics --- Intelligence, Artificial --- Intelligent machines --- Machine intelligence --- Thinking, Artificial --- Bionics --- Cognitive science --- Digital computer simulation --- Electronic data processing --- Logic machines --- Machine theory --- Self-organizing systems --- Simulation methods --- Fifth generation computers --- Neural computers --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Switching theory --- Informatics --- Science --- Computer software engineering --- Engineering --- Communication theory --- Communication --- Cybernetics
Choose an application
This volume is a self-contained introduction to interactive proof in high- order logic (HOL), using the proof assistant Isabelle 2002. Compared with existing Isabelle documentation, it provides a direct route into higher-order logic, which most people prefer these days. It bypasses ?rst-order logic and minimizes discussion of meta-theory. It is written for potential users rather than for our colleagues in the research world. Another departure from previous documentation is that we describe Markus Wenzel’s proof script notation instead of ML tactic scripts. The l- ter make it easier to introduce new tactics on the ?y, but hardly anybody does that. Wenzel’s dedicated syntax is elegant, replacing for example eight simpli?cation tactics with a single method, namely simp, with associated - tions. The book has three parts. – The ?rst part, Elementary Techniques, shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion. – The second part, Logic and Sets, presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes I- belle/HOL’s treatment of sets, functions, and relations and explains how to de?ne sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages.
Computer logic --- Automatic theorem proving --- Computer Science --- Engineering & Applied Sciences --- 681.3*D21 --- 681.3*D31 --- 681.3*F31 --- 681.3*F41 --- 681.3*I23 --- Automated theorem proving --- Theorem proving, Automated --- Theorem proving, Automatic --- Artificial intelligence --- Proof theory --- Computer science logic --- Logic, Symbolic and mathematical --- Requirements/specifications: languages; methodologies; tools (Software engineering)--See also {681.3*D31} --- Formal definitions and theory: semantics; syntax (Programming languages)--See also {681.3*D21}; {681.3*F31}; {681.3*F32}; {681.3*F42}; {681.3*F43} --- Specifying anf verifying and reasoning about programs: assertions; invariants; mechanical verification; pre- and post-conditions (Logics and meanings of programs)--See also {681.3*D21}; {681.3*D24}; {681.3*D31}; {681.3*E1} --- Mathematical logic: computability theory; computational logic; lambda calculus; logic programming; mechanical theorem proving; model theory; proof theory;recursive function theory--See also {681.3*F11}; {681.3*I22}; {681.3*I23} --- Deduction and theorem proving: answer/reason extraction; reasoning; resolution; metatheory; mathematical induction; logic programming (Artificial intelligence) --- 681.3*I23 Deduction and theorem proving: answer/reason extraction; reasoning; resolution; metatheory; mathematical induction; logic programming (Artificial intelligence) --- 681.3*F41 Mathematical logic: computability theory; computational logic; lambda calculus; logic programming; mechanical theorem proving; model theory; proof theory;recursive function theory--See also {681.3*F11}; {681.3*I22}; {681.3*I23} --- 681.3*F31 Specifying anf verifying and reasoning about programs: assertions; invariants; mechanical verification; pre- and post-conditions (Logics and meanings of programs)--See also {681.3*D21}; {681.3*D24}; {681.3*D31}; {681.3*E1} --- 681.3*D31 Formal definitions and theory: semantics; syntax (Programming languages)--See also {681.3*D21}; {681.3*F31}; {681.3*F32}; {681.3*F42}; {681.3*F43} --- 681.3*D21 Requirements/specifications: languages; methodologies; tools (Software engineering)--See also {681.3*D31} --- Computer logic. --- Automatic theorem proving. --- Computer science. --- Logic. --- Programming languages (Electronic computers). --- Computers. --- Mathematical logic. --- Artificial intelligence. --- Computer Science. --- Mathematical Logic and Formal Languages. --- Theory of Computation. --- Artificial Intelligence (incl. Robotics). --- Logics and Meanings of Programs. --- Programming Languages, Compilers, Interpreters. --- AI (Artificial intelligence) --- Artificial thinking --- Electronic brains --- Intellectronics --- Intelligence, Artificial --- Intelligent machines --- Machine intelligence --- Thinking, Artificial --- Bionics --- Cognitive science --- Digital computer simulation --- Electronic data processing --- Logic machines --- Machine theory --- Self-organizing systems --- Simulation methods --- Fifth generation computers --- Neural computers --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Automatic computers --- Automatic data processors --- Computer hardware --- Computing machines (Computers) --- Electronic calculating-machines --- Electronic computers --- Hardware, Computer --- Computer systems --- Cybernetics --- Calculators --- Cyberspace --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Languages, Artificial --- Argumentation --- Deduction (Logic) --- Deductive logic --- Dialectic (Logic) --- Logic, Deductive --- Intellect --- Philosophy --- Psychology --- Science --- Reasoning --- Thought and thinking --- Informatics --- Methodology --- Information theory. --- Logic design. --- Artificial Intelligence. --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Switching theory --- Communication theory --- Communication
Choose an application
Mathematical logic --- Computer science --- Programming --- Computer. Automation --- programmeren (informatica) --- programmeertalen --- wiskunde --- software engineering --- informatica management --- logica
Listing 1 - 10 of 19 | << page >> |
Sort by
|