×

Isar

swMATH ID: 4599
Software Authors: Makarius Wenzel
Description: Theorem proving system supporting both interactive proof development and some degree of automation have become quite successful in sizable applications in recent years (e.g. Isabelle/Bali or VerifiCard). Typical examples of this kind of semi-automated reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success in actually formalizing parts of mathematics and computer science, there are still obstacles in addressing a broad range of people. Paradoxically, none of the existing semi-automated reasoning systems have an adequate primary notion of proof that is amenable to human understanding (for communication, or just maintenance). The Intelligible semi-automated reasoning (Isar) approach to readable formal proof documents sets out to bridge the semantic gap between internal notions of proof given by state-of-the-art interactive theorem proving systems and an appropriate level of abstraction for user-level work. The Isar formal proof language has been designed to satisfy quite contradictory requirements, being both ’declarative’ and immediately ’executable’, by virtue of the Isar/VM interpreter. Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings: it is based on a few basic principles only, it is quite independent of the underlying logic, and integrates a broad range of automated proof methods. Interactive proof development is supported directly as well.
The Isabelle system offers Isar as an alternative proof language interface layer, beyond traditional tactic scripts. The Isabelle/Isar system provides an interpreter for the Isar formal proof document language. Isabelle/Isar input consists either of proper document constructors, or improper auxiliary commands (for diagnostics, exploration etc.). Proof texts consisting of proper document constructors only admit a purely static reading, thus being intelligible later without requiring dynamic replay that is so typical for traditional proof scripts. Any of the Isabelle/Isar commands may be executed in single-steps, so basically the interpreter has a proof text debugger already built-in.
The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably between Isabelle-classic proof scripts and Isabelle/Isar documents. Isar is as generic as Isabelle, able to support a wide range of object-logics. The current end-user setup is mainly for Isabelle/HOL.
Together with the Isabelle/Isar instantiation of Proof General, a generic (X)Emacs interface for interactive proof assistants, we arrive at a reasonable environment for live proof document editing. Thus proof texts may be developed incrementally by issuing proper document constructors, including forward and backward tracing of partial documents; intermediate states may be inspected by diagnostic commands.
Homepage: http://isabelle.in.tum.de/Isar/
Related Software: Isabelle; Isabelle/HOL; Coq; Mizar; Isabelle/Isar; HOL; Archive Formal Proofs; Sledgehammer; PVS; HOL Light; Proof General; ML; E Theorem Prover; VAMPIRE; z3; TPTP; Theorema; Metis_; OMDoc; SPASS
Cited in: 148 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Calculational reasoning revisited. An Isabelle/Isar experience. Zbl 1005.68535
Bauer, Gertrud; Wenzel, Markus
2001
all top 5

Cited by 226 Authors

9 Blanchette, Jasmin Christian
8 Nipkow, Tobias
8 Wenzel, Makarius
5 Pąk, Karol
4 Autexier, Serge
4 Ballarin, Clemens
4 Fleury, Mathias
4 Janičić, Predrag
4 Kaliszyk, Cezary
4 Korniłowicz, Artur
4 Narboux, Julien
4 Naumowicz, Adam
4 Paulson, Lawrence Charles
4 Popescu, Andrei
4 Sacerdoti Coen, Claudio
4 Urban, Josef
4 Wiedijk, Freek
3 Aspinall, David
3 Böhme, Sascha
3 Dietrich, Dominik
3 Fleuriot, Jacques D.
3 Geuvers, Jan Herman
3 Grabowski, Adam
3 Kunčar, Ondřej
3 Lammich, Peter
3 Maletzky, Alexander
3 Schlichtkrull, Anders
3 Tassi, Enrico
3 Traytel, Dmitry
3 Urban, Christian
3 Wolff, Burkhart
2 Aransay, Jesús
2 Arthan, Rob D.
2 Asperti, Andrea
2 Bengtson, Jesper
2 Bentkamp, Alexander
2 Benzmüller, Christoph Ewald
2 Berghofer, Stefan
2 Dixon, Lucas
2 Dufourd, Jean-François
2 Fiedler, Armin
2 Grov, Gudmund
2 Guttmann, Walter
2 Hupel, Lars
2 Kamareddine, Fairouz D.
2 Klakow, Dietrich
2 Koepke, Peter
2 Kühlwein, Daniel
2 Lamar, Robert
2 Li, Yongjian
2 Lyaletski, Alexander V.
2 Marić, Filip
2 Marmsoler, Diego
2 Obua, Steven
2 Pang, Jun
2 Parrow, Joachim
2 Paskevich, Andrei
2 Rabe, Florian
2 Rubio García, Julio Jesús
2 Schulz, Ewaryst
2 Sefidgar, S. Reza
2 Stojanović Đurđević, Sana
2 Stojanović, Sana
2 Sutcliffe, Geoff
2 Théry, Laurent
2 Verchinine, Konstantin
2 Wagner, Marc Oliver
2 Wells, Joe B.
2 Wenzel, Markus
1 Adamian, G. G.
1 Adams, Andrew A.
1 Alkassar, Eyad
1 Anisimov, Anatoly V.
1 Antonenko, N. V.
1 Avigad, Jeremy
1 Back, Ralph-Johan
1 Bancerek, Grzegorz
1 Barsotti, Damián
1 Bauer, Gertrud
1 Bauereiß, Thomas
1 Berghammer, Rudolf
1 Bezem, Marc
1 Biendarra, Julian
1 Billingsley, William
1 Bouzy, Aymeric
1 Brucker, Achim D.
1 Bulwahn, Lukas
1 Bundy, Alan
1 Butterfield, Andrew
1 Byliński, Czesław
1 Calude, Cristian S.
1 Chalin, Patrice
1 Chen, Ran
1 Chlipala, Adam J.
1 Churkin, A. V.
1 Cohen, Cyril
1 Colton, Simon
1 Corbineau, Pierre
1 Cramer, Marcos
1 Daumas, Marc
...and 126 more Authors
all top 5

Cited in 28 Serials

30 Journal of Automated Reasoning
7 Formal Aspects of Computing
5 Annals of Mathematics and Artificial Intelligence
3 Journal of Applied Logic
2 Theoretical and Mathematical Physics
2 Formal Methods in System Design
2 Mathematics in Computer Science
2 Logical Methods in Computer Science
1 Acta Informatica
1 International Journal of Theoretical Physics
1 Letters in Mathematical Physics
1 Mathematical Notes
1 Synthese
1 Journal of Symbolic Computation
1 Information and Computation
1 AI Communications
1 MSCS. Mathematical Structures in Computer Science
1 Informatica (Vilnius)
1 Foundations of Science
1 Concurrency and Computation: Practice & Experience
1 Sādhanā
1 Computer Languages, Systems & Structures
1 ACM Transactions on Computational Logic
1 Parallel Processing Letters
1 Lecture Notes in Computer Science
1 Journal of Formalized Reasoning
1 Frontiers of Computer Science
1 Journal of Logical and Algebraic Methods in Programming
all top 5

Cited in 21 Fields

140 Computer science (68-XX)
46 Mathematical logic and foundations (03-XX)
5 General and overarching topics; collections (00-XX)
4 Combinatorics (05-XX)
4 Quantum theory (81-XX)
3 Operations research, mathematical programming (90-XX)
2 Order, lattices, ordered algebraic structures (06-XX)
2 Commutative algebra (13-XX)
2 Numerical analysis (65-XX)
2 Relativity and gravitational theory (83-XX)
2 Information and communication theory, circuits (94-XX)
2 Mathematics education (97-XX)
1 Category theory; homological algebra (18-XX)
1 Group theory and generalizations (20-XX)
1 Partial differential equations (35-XX)
1 Functional analysis (46-XX)
1 Geometry (51-XX)
1 Manifolds and cell complexes (57-XX)
1 Probability theory and stochastic processes (60-XX)
1 Statistical mechanics, structure of matter (82-XX)
1 Game theory, economics, finance, and other social and behavioral sciences (91-XX)

Citations by Year