TY - BOOK ID - 2533308 TI - Isabelle : a generic theorem prover AU - Paulson, Lawrence C. AU - Nipkow, Tobias PY - 1994 VL - 828 SN - 3540582444 0387582444 3540485864 PB - Berlin ; New York ; Tokyo Springer-Verlag DB - UniCat KW - Automatic theorem proving KW - Theorema's--Automatische bewijsvoering KW - Théorèmes--Démonstration automatique KW - Automatic theorem proving. KW - Théorèmes KW - Démonstration automatique KW - Isabelle (Computer file) KW - Isabelle (Computer file). KW - Théorèmes KW - Démonstration automatique KW - Computer science. KW - Logic design. KW - Software engineering. KW - Artificial intelligence. KW - Logic, Symbolic and mathematical. KW - Mathematical Logic and Formal Languages. KW - Logics and Meanings of Programs. KW - Software Engineering. KW - Artificial Intelligence. KW - Mathematical Logic and Foundations. KW - Informatics KW - Science KW - AI (Artificial intelligence) KW - Artificial thinking KW - Electronic brains KW - Intellectronics KW - Intelligence, Artificial KW - Intelligent machines KW - Machine intelligence KW - Thinking, Artificial KW - Bionics KW - Cognitive science KW - Digital computer simulation KW - Electronic data processing KW - Logic machines KW - Machine theory KW - Self-organizing systems KW - Simulation methods KW - Fifth generation computers KW - Neural computers KW - Computer software engineering KW - Engineering KW - Design, Logic KW - Design of logic systems KW - Digital electronics KW - Electronic circuit design KW - Logic circuits KW - Switching theory KW - Algebra of logic KW - Logic, Universal KW - Mathematical logic KW - Symbolic and mathematical logic KW - Symbolic logic KW - Mathematics KW - Algebra, Abstract KW - Metamathematics KW - Set theory KW - Syllogism UR - https://www.unicat.be/uniCat?func=search&query=sysid:2533308 AB - As a generic theorem prover, Isabelle supports a variety of logics. Distinctive features include Isabelle's representation of logics within a meta-logic and the use of higher-order unification to combine inference rules. Isabelle can be applied to reasoning in pure mathematics or verification of computer systems. This volume constitutes the Isabelle documentation. It begins by outlining theoretical aspects and then demonstrates the use in practice. Virtually all Isabelle functions are described, with advice on correct usage and numerous examples. Isabelle's built-in logics are also described in detail. There is a comprehensive bebliography and index. The book addresses prospective users of Isabelle as well as researchers in logic and automated reasoning. ER -