1.1 --- a/src/Doc/Tutorial/document/rules.tex Mon Nov 25 14:50:31 2013 +0000
1.2 +++ b/src/Doc/Tutorial/document/rules.tex Mon Nov 25 16:00:09 2013 +0000
1.3 @@ -1,4 +1,4 @@
1.4 -%!TEX root = ../tutorial.tex
1.5 +%!TEX root = root.tex
1.6 \chapter{The Rules of the Game}
1.7 \label{chap:rules}
1.8
1.9 @@ -33,6 +33,8 @@
1.10 one symbol only. For predicate logic this can be
1.11 done, but when users define their own concepts they typically
1.12 have to refer to other symbols as well. It is best not to be dogmatic.
1.13 +Our system is not based on pure natural deduction, but includes elements from the sequent calculus
1.14 +and free-variable tableaux.
1.15
1.16 Natural deduction generally deserves its name. It is easy to use. Each
1.17 proof step consists of identifying the outermost symbol of a formula and
1.18 @@ -240,13 +242,14 @@
1.19 of a conjunction. Rules of this sort (where the conclusion is a subformula of a
1.20 premise) are called \textbf{destruction} rules because they take apart and destroy
1.21 a premise.%
1.22 -\footnote{This Isabelle terminology has no counterpart in standard logic texts,
1.23 +\footnote{This Isabelle terminology is not used in standard logic texts,
1.24 although the distinction between the two forms of elimination rule is well known.
1.25 Girard \cite[page 74]{girard89},\index{Girard, Jean-Yves|fnote}
1.26 for example, writes ``The elimination rules
1.27 [for $\disj$ and $\exists$] are very
1.28 bad. What is catastrophic about them is the parasitic presence of a formula [$R$]
1.29 -which has no structural link with the formula which is eliminated.''}
1.30 +which has no structural link with the formula which is eliminated.''
1.31 +These Isabelle rules are inspired by the sequent calculus.}
1.32
1.33 The first proof step applies conjunction introduction, leaving
1.34 two subgoals:
2.1 --- a/src/Doc/manual.bib Mon Nov 25 14:50:31 2013 +0000
2.2 +++ b/src/Doc/manual.bib Mon Nov 25 16:00:09 2013 +0000
2.3 @@ -194,7 +194,7 @@
2.4 @incollection{basin91,
2.5 author = {David Basin and Matt Kaufmann},
2.6 title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
2.7 - Comparison},
2.8 + Comparison},
2.9 crossref = {huet-plotkin91},
2.10 pages = {89-119}}
2.11
2.12 @@ -472,7 +472,7 @@
2.13 @book{constable86,
2.14 author = {R. L. Constable and others},
2.15 title = {Implementing Mathematics with the Nuprl Proof
2.16 - Development System},
2.17 + Development System},
2.18 publisher = Prentice,
2.19 year = 1986}
2.20
2.21 @@ -505,7 +505,7 @@
2.22 @incollection{dybjer91,
2.23 author = {Peter Dybjer},
2.24 title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type
2.25 - Theory and Their Set-Theoretic Semantics},
2.26 + Theory and Their Set-Theoretic Semantics},
2.27 crossref = {huet-plotkin91},
2.28 pages = {280-306}}
2.29
2.30 @@ -533,7 +533,7 @@
2.31 @InProceedings{felty91a,
2.32 Author = {Amy Felty},
2.33 Title = {A Logic Program for Transforming Sequent Proofs to Natural
2.34 - Deduction Proofs},
2.35 + Deduction Proofs},
2.36 crossref = {extensions91},
2.37 pages = {157-178}}
2.38
2.39 @@ -566,9 +566,9 @@
2.40
2.41 @inproceedings{OBJ,
2.42 author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
2.43 - and J. Meseguer},
2.44 + and J. Meseguer},
2.45 title = {Principles of {OBJ2}},
2.46 - booktitle = POPL,
2.47 + booktitle = POPL,
2.48 year = 1985,
2.49 pages = {52-66}}
2.50
2.51 @@ -576,7 +576,7 @@
2.52
2.53 @book{gallier86,
2.54 author = {J. H. Gallier},
2.55 - title = {Logic for Computer Science:
2.56 + title = {Logic for Computer Science:
2.57 Foundations of Automatic Theorem Proving},
2.58 year = 1986,
2.59 publisher = {Harper \& Row}}
2.60 @@ -605,8 +605,8 @@
2.61 author = {Jean-Yves Girard},
2.62 title = {Proofs and Types},
2.63 year = 1989,
2.64 - publisher = CUP,
2.65 - note = {Translated by Yves LaFont and Paul Taylor}}
2.66 + publisher = CUP,
2.67 + note = {Translated by Yves Lafont and Paul Taylor}}
2.68
2.69 @Book{mgordon-hol,
2.70 editor = {M. J. C. Gordon and T. F. Melham},
2.71 @@ -777,21 +777,21 @@
2.72
2.73 @article{huet78,
2.74 author = {G. P. Huet and B. Lang},
2.75 - title = {Proving and Applying Program Transformations Expressed with
2.76 + title = {Proving and Applying Program Transformations Expressed with
2.77 Second-Order Patterns},
2.78 journal = acta,
2.79 volume = 11,
2.80 - year = 1978,
2.81 + year = 1978,
2.82 pages = {31-55}}
2.83
2.84 @inproceedings{huet88,
2.85 author = {G{\'e}rard Huet},
2.86 title = {Induction Principles Formalized in the {Calculus of
2.87 - Constructions}},
2.88 + Constructions}},
2.89 booktitle = {Programming of Future Generation Computers},
2.90 editor = {K. Fuchi and M. Nivat},
2.91 year = 1988,
2.92 - pages = {205-216},
2.93 + pages = {205-216},
2.94 publisher = {Elsevier}}
2.95
2.96 @inproceedings{Huffman-Kuncar:2013:lifting_transfer,
2.97 @@ -843,7 +843,7 @@
2.98 %K
2.99
2.100 @InProceedings{kammueller-locales,
2.101 - author = {Florian Kamm{\"u}ller and Markus Wenzel and
2.102 + author = {Florian Kamm{\"u}ller and Markus Wenzel and
2.103 Lawrence C. Paulson},
2.104 title = {Locales: A Sectioning Concept for {Isabelle}},
2.105 crossref = {tphols99}}
2.106 @@ -944,7 +944,7 @@
2.107 author = {Gavin Lowe},
2.108 title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
2.109 Protocol using {CSP} and {FDR}},
2.110 - booktitle = {Tools and Algorithms for the Construction and Analysis
2.111 + booktitle = {Tools and Algorithms for the Construction and Analysis
2.112 of Systems: second international workshop, TACAS '96},
2.113 editor = {T. Margaria and B. Steffen},
2.114 series = {LNCS 1055},
2.115 @@ -978,7 +978,7 @@
2.116 @incollection{melham89,
2.117 author = {Thomas F. Melham},
2.118 title = {Automating Recursive Type Definitions in Higher Order
2.119 - Logic},
2.120 + Logic},
2.121 pages = {341-386},
2.122 crossref = {birtwistle89}}
2.123
2.124 @@ -1057,7 +1057,7 @@
2.125
2.126 @InProceedings{NaraschewskiW-TPHOLs98,
2.127 author = {Wolfgang Naraschewski and Markus Wenzel},
2.128 - title =
2.129 + title =
2.130 {Object-Oriented Verification based on Record Subtyping in
2.131 Higher-Order Logic},
2.132 crossref = {tphols98}}
2.133 @@ -1190,8 +1190,8 @@
2.134 @book{nordstrom90,
2.135 author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
2.136 title = {Programming in {Martin-L{\"o}f}'s Type Theory. An
2.137 - Introduction},
2.138 - publisher = {Oxford University Press},
2.139 + Introduction},
2.140 + publisher = {Oxford University Press},
2.141 year = 1990}
2.142
2.143 %O
2.144 @@ -1251,7 +1251,7 @@
2.145 @InProceedings{paulson-COLOG,
2.146 author = {Lawrence C. Paulson},
2.147 title = {A Formulation of the Simple Theory of Types (for
2.148 - {Isabelle})},
2.149 + {Isabelle})},
2.150 pages = {246-274},
2.151 crossref = {colog88},
2.152 url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
2.153 @@ -1304,7 +1304,7 @@
2.154 %replaces paulson-final
2.155 @Article{paulson-mscs,
2.156 author = {Lawrence C. Paulson},
2.157 - title = {Final Coalgebras as Greatest Fixed Points
2.158 + title = {Final Coalgebras as Greatest Fixed Points
2.159 in {ZF} Set Theory},
2.160 journal = {Mathematical Structures in Computer Science},
2.161 year = 1999,
2.162 @@ -1337,9 +1337,9 @@
2.163 crossref = {milner-fest}}
2.164
2.165 @book{milner-fest,
2.166 - title = {Proof, Language, and Interaction:
2.167 + title = {Proof, Language, and Interaction:
2.168 Essays in Honor of {Robin Milner}},
2.169 - booktitle = {Proof, Language, and Interaction:
2.170 + booktitle = {Proof, Language, and Interaction:
2.171 Essays in Honor of {Robin Milner}},
2.172 publisher = MIT,
2.173 year = 2000,
2.174 @@ -1427,7 +1427,7 @@
2.175 @book{paulson87,
2.176 author = {Lawrence C. Paulson},
2.177 title = {Logic and Computation: Interactive proof with Cambridge
2.178 - LCF},
2.179 + LCF},
2.180 year = 1987,
2.181 publisher = CUP}
2.182
2.183 @@ -1470,7 +1470,7 @@
2.184 @article{pelletier86,
2.185 author = {F. J. Pelletier},
2.186 title = {Seventy-five Problems for Testing Automatic Theorem
2.187 - Provers},
2.188 + Provers},
2.189 journal = JAR,
2.190 volume = 2,
2.191 pages = {191-216},
2.192 @@ -1486,13 +1486,13 @@
2.193 publisher = CUP,
2.194 year = 1993}
2.195
2.196 -@Article{pitts94,
2.197 +@Article{pitts94,
2.198 author = {Andrew M. Pitts},
2.199 title = {A Co-induction Principle for Recursively Defined Domains},
2.200 journal = TCS,
2.201 - volume = 124,
2.202 + volume = 124,
2.203 pages = {195-219},
2.204 - year = 1994}
2.205 + year = 1994}
2.206
2.207 @Article{plaisted90,
2.208 author = {David A. Plaisted},
2.209 @@ -1561,7 +1561,7 @@
2.210 @inproceedings{saaltink-fme,
2.211 author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
2.212 Dan Craigen and Irwin Meisels},
2.213 - title = {An {EVES} Data Abstraction Example},
2.214 + title = {An {EVES} Data Abstraction Example},
2.215 pages = {578-596},
2.216 crossref = {fme93}}
2.217
2.218 @@ -1897,7 +1897,7 @@
2.219 author = {A. N. Whitehead and B. Russell},
2.220 title = {Principia Mathematica},
2.221 year = 1962,
2.222 - publisher = CUP,
2.223 + publisher = CUP,
2.224 note = {Paperback edition to *56,
2.225 abridged from the 2nd edition (1927)}}
2.226
2.227 @@ -1982,9 +1982,9 @@
2.228 @book{birtwistle89,
2.229 editor = {Graham Birtwistle and P. A. Subrahmanyam},
2.230 title = {Current Trends in Hardware Verification and Automated
2.231 - Theorem Proving},
2.232 + Theorem Proving},
2.233 booktitle = {Current Trends in Hardware Verification and Automated
2.234 - Theorem Proving},
2.235 + Theorem Proving},
2.236 publisher = {Springer},
2.237 year = 1989}
2.238
2.239 @@ -1997,9 +1997,9 @@
2.240
2.241 @Proceedings{cade12,
2.242 editor = {Alan Bundy},
2.243 - title = {Automated Deduction --- {CADE}-12
2.244 + title = {Automated Deduction --- {CADE}-12
2.245 International Conference},
2.246 - booktitle = {Automated Deduction --- {CADE}-12
2.247 + booktitle = {Automated Deduction --- {CADE}-12
2.248 International Conference},
2.249 year = 1994,
2.250 series = {LNAI 814},
2.251 @@ -2059,7 +2059,7 @@
2.252 title = {Extensions of Logic Programming},
2.253 booktitle = {Extensions of Logic Programming},
2.254 year = 1991,
2.255 - series = {LNAI 475},
2.256 + series = {LNAI 475},
2.257 publisher = {Springer}}
2.258
2.259 @proceedings{cade10,
2.260 @@ -2078,9 +2078,9 @@
2.261 year = 1993}
2.262
2.263 @book{wos-fest,
2.264 - title = {Automated Reasoning and its Applications:
2.265 + title = {Automated Reasoning and its Applications:
2.266 Essays in Honor of {Larry Wos}},
2.267 - booktitle = {Automated Reasoning and its Applications:
2.268 + booktitle = {Automated Reasoning and its Applications:
2.269 Essays in Honor of {Larry Wos}},
2.270 publisher = MIT,
2.271 year = 1997,