/
bib-joehurd.bib
3985 lines (3630 loc) · 143 KB
/
bib-joehurd.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
@INPROCEEDINGS{aagaard1998,
AUTHOR = {Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger},
TITLE = {Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment},
PAGES = {538--541},
BOOKTITLE = {Proceedings of the 1998 Conference on Design Automation ({DAC}-98)},
MONTH = JUN,
PUBLISHER = {ACM/IEEE},
ADDRESS = {Los Alamitos, CA},
YEAR = 1998
}
@ARTICLE{abadi1994,
AUTHOR = {Martin Abadi and Joseph Y. Halpern},
TITLE = {Decidability and expressiveness for first-order logics of probability},
JOURNAL = {Information and Computation},
YEAR = 1994
}
@BOOK{ackermann1954,
AUTHOR = {Wilhelm Ackermann},
TITLE = {Solvable Cases of the Decision Problem},
PUBLISHER = {North-Holland},
SERIES = {Studies in Logic and the Foundations of Mathematics},
ADDRESS = {Amsterdam},
YEAR = 1954
}
@INCOLLECTION{ahrendt1998,
AUTHOR = {Wolfgang Ahrendt and Bernhard Beckert and Reiner H{\"a}hnle and Wolfram Menzel and Wolfgang Reif and Gerhard Schellhorn and Peter H. Schmitt},
TITLE = {Integration of Automated and Interactive Theorem Proving},
PUBLISHER = {Kluwer},
BOOKTITLE = {Automated Deduction: A Basis for Applications},
EDITOR = {W. Bibel and P. Schmitt},
YEAR = 1998,
VOLUME = {II},
CHAPTER = {4},
PAGES = {97--116},
URL = {http://i11www.ira.uka.de/~ahrendt/papers/intDfgPaper.ps.gz},
ABSTRACT = {In this chapter we present a project to integrate interactive and
automated theorem proving. Its aim is to combine the advantages of the
two paradigms. We focus on one particular application domain, which is
deduction for the purpose of software verification. Some of the
reported facts may not be valid in other domains. We report on the
integration concepts and on the experimental results with a prototype
implementation.}
}
@INPROCEEDINGS{armando1998,
AUTHOR = {A. Armando and S. Ranise},
TITLE = {From Integrated Reasoning Specialists to ``Plug-and-Play'' Reasoning Components},
PAGES = {42--54},
CROSSREF = {aisc1998}
}
@ARTICLE{armando2002,
AUTHOR = {Alessandro Armando and Silvio Ranise and Michael Rusinowitch},
TITLE = {A Rewriting Approach to Satisfiability Procedures},
JOURNAL = {Information and Computation},
NOTE = {To appear},
URL = {http://www.loria.fr/~rusi/pub/longcsl01.ps}
}
@INPROCEEDINGS{astrachan1992,
AUTHOR = {Owen L. Astrachan and Mark E. Stickel},
TITLE = {Caching and Lemmaizing in Model Elimination Theorem Provers},
PAGES = {224--238},
CROSSREF = {cade1992},
URL = {http://www.cs.duke.edu/~ola/meteor.html}
}
@ARTICLE{astrachan1997,
TITLE = {The Use of Lemmas in the Model Elimination Procedure},
AUTHOR = {O. L. Astrachan and Donald W. Loveland},
JOURNAL = {Journal of Automated Reasoning},
PAGES = {117--141},
MONTH = AUG,
YEAR = 1997,
VOLUME = 19,
NUMBER = 1,
URL = {http://www.cs.duke.edu/~ola/meteor.html}
}
@BOOK{baader1998,
AUTHOR = {Franz Baader and Tobias Nipkow},
TITLE = {Term Rewriting and All That},
PUBLISHER = {Cambridge University Press},
YEAR = 1998
}
@BOOK{baker1984,
AUTHOR = {Alan Baker},
TITLE = {A Concise Introduction to the Theory of Numbers},
PUBLISHER = {Cambridge University Press},
YEAR = 1984
}
@INPROCEEDINGS{baker1992,
AUTHOR = {Siani Baker and Andrew Ireland and Alan Smaill},
TITLE = {On the Use of the Constructive Omega-Rule Within Automated Deduction},
PAGES = {214--225},
CROSSREF = {lpar1992},
URL = {http://www.dai.ed.ac.uk/papers/documents/rp560.html},
ABSTRACT = {The cut elimination theorem for predicate calculus states that every
proof may be replaced by one which does not involve use of the cut
rule. This theorem no longer holds when the system is extended with
Peano's axioms to give a formalisation for arithmetic. The problem of
generalisation results, since arbitrary formulae can be cut in. This
makes theorem-proving very difficult - one solution is to embed
arithmetic in a stronger system, where cut elimination holds. This
paper describes a system based on the omega rule, and shows that
certain statements are provable in this system which are not provable
in Peano arithmetic without cut. Moreover, an important application is
presented in the form of a new method of generalisation by means of
"guiding proofs" in the stronger system, which sometimes succeeds in
producing proofs in the original system when other methods fail. The
implementation of such a system is also described.}
}
@ARTICLE{bancerek1989,
AUTHOR = {Grzegorz Bancerek},
TITLE = {The Fundamental Properties of Natural Numbers},
JOURNAL = {Journal of Formalized Mathematics},
VOLUME = {1},
YEAR = 1989
}
@BOOK{bardell1987,
AUTHOR = {Paul H. Bardell and W. H. McAnney and J. Savir},
TITLE = {Built In Test for {VLSI}: Pseudorandom Techniques},
PUBLISHER = {John Wiley},
MONTH = OCT,
YEAR = 1987,
URL = {http://www.wiley.com/Corporate/Website/Objects/Products/0,9049,65654,00.html},
ABSTRACT = {This handbook provides ready access to all of the major concepts,
techniques, problems, and solutions in the emerging field of
pseudorandom pattern testing. Until now, the literature in this area
has been widely scattered, and published work, written by
professionals in several disciplines, has treated notation and
mathematics in ways that vary from source to source. This book opens
with a clear description of the shortcomings of conventional testing
as applied to complex digital circuits, revewing by comparison the
principles of design for testability of more advanced digital
technology. Offers in-depth discussions of test sequence generation
and response data compression, including pseudorandom sequence
generators; the mathematics of shift-register sequences and their
potential for built-in testing. Also details random and memory testing
and the problems of assessing the efficiency of such tests, and the
limitations and practical concerns of built-in testing.}
}
@TECHREPORT{barras1997,
TITLE = {The {Coq} Proof Assistant Reference Manual: Version 6.1},
AUTHOR = {Bruno Barras and Samuel Boutin and Cristina Cornes and Judicael Courant and Jean-Christophe Filliatre and Eduardo Gimenez and Hugo Herbelin and G{\'e}rard Huet and C{\'{e}}sar A. Mu{\~{n}}oz and Chetan Murthy and Catherine Parent and Christine Paulin-Mohring and Amokrane Saibi and Benjamin Werner},
TYPE = {Technical Report},
INSTITUTION = {INRIA (Institut National de Recherche en Informatique et en Automatique), France},
NUMBER = {RT-0203},
YEAR = 1997
}
@INPROCEEDINGS{barras2000,
AUTHOR = {Bruno Barras},
TITLE = {Programming and Computing in {HOL}},
PAGES = {17--37},
CROSSREF = {tphols2000}
}
@ARTICLE{beckert1995,
AUTHOR = {Bernhard Beckert and Joachim Posegga},
TITLE = {{leanTAP}: Lean Tableau-based Deduction},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = 15,
NUMBER = 3,
PAGES = {339--358},
MONTH = DEC,
YEAR = 1995,
URL = {ftp://i12ftp.ira.uka.de/pub/posegga/LeanTaP.color.ps.Z},
ABSTRACT = { prove((E,F),A,B,C,D) :- !,prove(E,[F|A],B,C,D).
prove((E;F),A,B,C,D) :- !,prove(E,A,B,C,D),prove(F,A,B,C,D).
prove(all(I,J),A,B,C,D) :- !,
\+length(C,D),copy_term((I,J,C),(G,F,C)),
append(A,[all(I,J)],E),prove(F,E,B,[G|C],D).
prove(A,_,[C|D],_,_) :-
((A= -(B);-(A)=B) -> (unify(B,C);prove(A,[],D,_,_))).
prove(A,[E|F],B,C,D) :- prove(E,F,[A|B],C,D).
implements a first-order theorem prover based on free-variable semantic
tableaux. It is complete, sound, and efficient.}
}
@BOOK{beeson1985,
AUTHOR = {Michael J. Beeson},
TITLE = {Foundations of Constructive Mathematics},
PUBLISHER = {Springer},
YEAR = 1985
}
@INPROCEEDINGS{beeson1998,
AUTHOR = {Michael Beeson},
TITLE = {Unification in {Lambda-Calculi} with if-then-else},
PAGES = {103--118},
CROSSREF = {cade1998},
URL = {http://link.springer-ny.com/link/service/series/0558/bibs/1421/14210103.htm},
ABSTRACT = {A new unification algorithm is introduced, which (unlike previous
algorithms for unification in $lambda$-calculus) shares the pleasant
properties of first-order unification. Proofs of these properties are
given, in particular uniqueness of the answer and the
most-general-unifier property. This unification algorithm can be used
to generalize first-order proof-search algorithms to second-order
logic, making possible for example a straighforward treatment of
McCarthy's circumscription schema.}
}
@BOOK{bell1930,
AUTHOR = {Eric T. Bell},
TITLE = {Debunking Science},
PUBLISHER = {University of Washington Book Store},
YEAR = 1930
}
@PHDTHESIS{benzmuller1999,
AUTHOR = {C. Benzmuller},
TITLE = {Equality and Extensionality in Higher-Order Theorem Proving},
SCHOOL = {Saarland University},
MONTH = APR,
YEAR = 1999,
URL = {http://www.ags.uni-sb.de/~chris/papers/diss.ps.gz}
}
@ARTICLE{berlekamp1970,
AUTHOR = {E. R. Berlekamp},
TITLE = {Factoring polynomials over large finite fields},
JOURNAL = {Math. Comput.},
VOLUME = 24,
YEAR = 1970,
PAGE = {713--735},
ABSTRACT = {"This paper presents algorithms for root-finding and factorization,
two problems in finite fields. The latter problem is reduced to the
root-finding problem, for which a probabilistic algorithm is
given. This paper is a precursor of Rabin (1980)."}
}
@INPROCEEDINGS{bezem2000,
AUTHOR = {Marc Bezem and Dimitri Hendriks and Hans de Nivelle},
TITLE = {Automated Proof Construction in Type Theory Using Resolution},
PAGES = {148--163},
CROSSREF = {cade2000},
URL = {http://www.phil.uu.nl/~hendriks/}
}
@ARTICLE{bialas1990,
AUTHOR = {J\'ozef Bia{\l}as},
TITLE = {The $\sigma$-additive Measure Theory},
JOURNAL = {Journal of Formalized Mathematics},
YEAR = {1990},
URL = {http://mizar.uwb.edu.pl/JFM/Vol2/measure1.html}
}
@ARTICLE{bialas1992,
AUTHOR = {J\'ozef Bia{\l}as},
TITLE = {Properties of {Caratheodor}'s Measure},
JOURNAL = {Journal of Formalized Mathematics},
YEAR = {1992},
URL = {http://mizar.uwb.edu.pl/JFM/Vol4/measure4.html}
}
@BOOK{bierce1911,
AUTHOR = {Ambrose Bierce},
TITLE = {The Devil's Dictionary},
PUBLISHER = {Dover},
EDITION = {Dover thrift},
YEAR = 1993
}
@INBOOK{biere2003,
AUTHOR = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Ofer Strichman and Yunshun Zhu},
TITLE = {Bounded Model Checking},
CHAPTER = {},
SERIES = {Advances in Computers},
VOLUME = 58,
PUBLISHER = {Elsevier},
YEAR = 2003,
NOTE = {To appear},
URL = {http://www-2.cs.cmu.edu/~ofers/advances.pdf}
}
@BOOK{billingsley1986,
AUTHOR = {P. Billingsley},
TITLE = {Probability and Measure},
EDITION = {2nd},
PUBLISHER = {John Wiley \& Sons, Inc.},
ADDRESS = {New York},
YEAR = 1986
}
@UNPUBLISHED{bishop2004,
AUTHOR = {Steven Bishop and Matthew Fairbairn and Michael Norrish and Peter Sewell and Keith Wansbrough},
TITLE = {The {TCP} Specification: A Quick Introduction},
NOTE = {Available from Peter Sewell's web site},
MONTH = MAR,
YEAR = 2004,
URL = {http://www.cl.cam.ac.uk/~pes20/Netsem/quickstart.ps}
}
@BOOK{boole1847,
AUTHOR = {George Boole},
TITLE = {The Mathematical Analysis of Logic, Being an Essay Toward a Calculus of Deductive Reasoning},
ADDRESS = {Cambridge},
PUBLISHER = {Macmillan},
YEAR = 1847,
PAGES = 82
}
@ARTICLE{boulton1993,
AUTHOR = {Richard J. Boulton},
TITLE = {Lazy Techniques for Fully Expansive Theorem Proving},
JOURNAL = {Formal Methods in System Design},
YEAR = 1993,
VOLUME = 3,
NUMBER = {1/2},
PAGES = {25--47},
MONTH = AUG
}
@INPROCEEDINGS{boulton1995,
AUTHOR = {Richard J. Boulton},
TITLE = {Combining Decision Procedures in the {HOL} System},
PAGES = {75--89},
CROSSREF = {tphols1995}
}
@ARTICLE{boyer1984,
AUTHOR = {Robert S. Boyer and J Strother Moore},
TITLE = {Proof checking the {RSA} public key encryption algorithm},
JOURNAL = {American Mathematical Monthly},
VOLUME = 91,
NUMBER = 3,
PAGES = {181--189},
YEAR = 1984,
URL = {http://www.cs.utexas.edu/users/boyer/rsa.ps.Z}
}
@ARTICLE{boyer1988,
AUTHOR = {Robert S. Boyer and J Strother Moore},
TITLE = {Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic},
JOURNAL = {Machine Intelligence},
VOLUME = {11},
PUBLISHER = {Oxford University Press},
YEAR = 1988,
PAGES = {83-124}
}
@INPROCEEDINGS{boyer1994,
AUTHOR = {Robert S. Boyer and N. G. de Bruijn and G{\'e}rard Huet and Andrzej Trybulec},
TITLE = {A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?},
PAGES = {237--251},
CROSSREF = {cade1994}
}
@UNPUBLISHED{bundy1996,
AUTHOR = {Alan Bundy},
TITLE = {Artificial Mathematicians},
NOTE = {Available from the author's web site},
MONTH = MAY,
YEAR = 1996,
URL = {http://www.dai.ed.ac.uk/homes/bundy/tmp/new-scientist.ps.gz}
}
@INPROCEEDINGS{debruijn1970,
AUTHOR = {N. de Bruijn},
TITLE = {The Mathematical language {AUTOMATH}, its usage, and some of its extensions},
BOOKTITLE = {Symposium on Automatic Demonstration},
ORGANIZATION = {Lecture Notes in Mathematics, 125},
PUBLISHER = {Springer},
PAGES = {29--61},
YEAR = 1970
}
@ARTICLE{buffon1777,
AUTHOR = {G. Buffon},
TITLE = {Essai d'arithm\'etique morale},
JOURNAL = {Suppl\'ement \`a l'Histoire Naturelle},
VOLUME = 4,
YEAR = 1777
}
@BOOK{bundy1983,
AUTHOR = {Alan Bundy},
TITLE = {The Computer Modelling of Mathematical Reasoning},
PUBLISHER = {Academic Press},
YEAR = 1983
}
@ARTICLE{burrows1990,
AUTHOR = {Michael Burrows and Mart{\'\i}n Abadi and Roger Needham},
TITLE = {A Logic of Authentication},
JOURNAL = {ACM Transactions on Computer Systems},
VOLUME = 8,
YEAR = 1990,
PAGES = {18--36},
NUMBER = 1,
MONTH = FEB,
URL = {http://www.acm.org/pubs/articles/journals/tocs/1990-8-1/p18-burrows/p18-burrows.pdf},
ABSTRACT = {Authentication protocols are the basis of security in many
distributed systems, and it is therefore essential to ensure that
these protocols function correctly. Unfortunately, their design has
been extremely error prone. Most of the protocols found in the
literature contain redundancies or security flaws. A simple logic has
allowed us to describe the beliefs of trustworthy parties involved in
authentication protocols and the evolution of these beliefs as a
consequence of communication. We have been able to explain a variety
of authentication protocols formally, to discover subtleties and
errors in them, and to suggest improvements. In this paper we present
the logic and then give the results of our analysis of four published
protocols, chosen either because of their practical importance or
because they serve to illustrate our method.}
}
@ARTICLE{burstall1977,
AUTHOR = {Rod Burstall and John Darlington},
TITLE = {A transformation system for developing recursive programs},
JOURNAL = {Journal of the Association for Computing Machinery},
VOLUME = {1},
MONTH = JAN,
YEAR = 1977
}
@INPROCEEDINGS{busch1994,
AUTHOR = {H. Busch},
TITLE = {First-Order Automation for Higher-Order-Logic Theorem Proving},
CROSSREF = {tphols1994}
}
@ARTICLE{caprotti2001,
AUTHOR = {O. Caprotti and M. Oostdijk},
TITLE = {Formal and Efficient Primality Proofs by use of Computer Algebra Oracles},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = 32,
NUMBER = {1--2},
PAGES = {55--70},
YEAR = 2001,
EDITOR = {T. Recio and M. Kerber},
NOTE = {Special Issue on Computer Algebra and Mechanized Reasoning}
}
@BOOK{chang1973,
AUTHOR = {Chin-Liang Chang and Richard Char-Tung Lee},
TITLE = {Symbolic Logic and Mechanical Theorem Proving},
PUBLISHER = {Academic Press},
ADDRESS = {New York},
YEAR = 1973
}
@ARTICLE{church1940,
AUTHOR = {Alonzo Church},
TITLE = {A Formulation of the Simple Theory of Types},
JOURNAL = {Journal of Symbolic Logic},
YEAR = 1940,
VOLUME = 5,
PAGES = {56--68}
}
@ARTICLE{claessen2000,
AUTHOR = {Koen Claessen and John Hughes},
TITLE = {{QuickCheck}: a lightweight tool for random testing of {Haskell} programs},
JOURNAL = {ACM SIG{\-}PLAN Notices},
VOLUME = {35},
NUMBER = {9},
PAGES = {268--279},
MONTH = SEP,
YEAR = {2000},
URL = {http://www.md.chalmers.se/~rjmh/QuickCheck/}
}
@BOOK{clarke1999,
AUTHOR = {E. M. Clarke and O. Grumberg and D. A. Peled},
TITLE = {{M}odel {C}hecking},
PUBLISHER = {The MIT Press},
YEAR = {1999}
}
@INPROCEEDINGS{colwell2000,
AUTHOR = {Bob Colwell and Bob Brennan},
TITLE = {Intel's Formal Verification Experience on the {Willamette} Development},
PAGES = {106--107},
CROSSREF = {tphols2000}
}
@PHDTHESIS{compagnoni1995,
AUTHOR = {Adriana B. Compagnoni},
TITLE = {Higher-Order Subtyping with Intersection Types},
YEAR = 1995,
MONTH = JAN,
SCHOOL = {Catholic University, Nigmegen}
}
@INPROCEEDINGS{cook1971,
AUTHOR = {Stephen A. Cook},
TITLE = {The complexity of theorem-proving procedures},
PAGES = {151--158},
EDITOR = {{ACM}},
BOOKTITLE = {Third annual {ACM} Symposium on Theory of Computing},
ADDRESS = {Shaker Heights, Ohio, USA},
MONTH = MAY,
YEAR = 1971,
PUBLISHER = {ACM Press}
}
@UNPUBLISHED{cook2000,
AUTHOR = {Stephen A. Cook},
TITLE = {The {P} Versus {NP} Problem},
MONTH = APR,
YEAR = 2000,
NOTE = {Manuscript prepared for the Clay Mathematics Institute for the Millennium Prize Problems},
URL = {http://www.claymath.org/prizeproblems/pvsnp.htm}
}
@BOOK{cormen1990,
AUTHOR = {Thomas H. Cormen and Charles Eric Leiserson and Ronald L. Rivest},
TITLE = {Introduction to Algorithms},
PUBLISHER = {MIT Press/McGraw-Hill},
ADDRESS = {Cambridge, Massachusetts},
YEAR = 1990
}
@TECHREPORT{curzon1994,
AUTHOR = {Paul Curzon},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = MAR,
NUMBER = {328},
TITLE = {The formal verification of the {Fairisle} {ATM} switching element: an overview},
YEAR = 1994
}
@INPROCEEDINGS{cyrluk1996,
AUTHOR = {David Cyrluk and Patrick Lincoln and Natarajan Shankar},
TITLE = {On {Shostak}'s Decision Procedure for Combinations of Theories},
CROSSREF = {cade1996}
}
@INPROCEEDINGS{dahn1997,
AUTHOR = {Ingo Dahn and Christoph Wernhard},
TITLE = {First Order Proof Problems Extracted from an Article in the {MIZAR} Mathematical Library},
CROSSREF = {ftp1997},
URL = {http://www-irm.mathematik.hu-berlin.de/~ilf/papers/index.html}
}
@INPROCEEDINGS{dahn1998,
TITLE = {Interpretation of a {Mizar}-like logic in first-order logic},
AUTHOR = {Ingo Dahn},
PAGES = {116--126},
CROSSREF = {ftp1998}
}
@BOOK{davenport1992,
AUTHOR = {Harold Davenport},
TITLE = {The Higher Arithmetic},
PUBLISHER = {Cambridge University Press},
YEAR = 1992,
EDITION = {Sixth}
}
@BOOK{degroot1989,
AUTHOR = {Morris DeGroot},
TITLE = {Probability and Statistics},
PUBLISHER = {Addison-Wesley},
EDITION = {2nd},
YEAR = 1989
}
@INCOLLECTION{deleeuw1955,
AUTHOR = {K. de Leeuw and E. F. Moore and C. E. Shannon and N. Shapiro},
TITLE = {Computability by probabilistic machines},
PAGES = {183--212},
BOOKTITLE = {Automata Studies},
EDITOR = {C. E. Shannon and J. McCarthy},
YEAR = 1955,
PUBLISHER = {Princeton University Press},
ADDRESS = {Princeton, NJ}
}
@TECHREPORT{denzinger1997,
AUTHOR = {J{\"o}rg Denzinger and Dirk Fuchs},
TITLE = {Knowledge-based Cooperation between Theorem Provers by {TECHS}},
YEAR = 1997,
TYPE = {SEKI-Report},
NUMBER = {SR-97-11},
INSTITUTION = {University of Kaiserslautern},
URL = {http://agent.informatik.uni-kl.de/seki/1997/Fuchs.SR-97-11.ps.gz}
}
@BOOK{dijkstra1976,
AUTHOR = {E. W. Dijkstra},
TITLE = {A Discipline of Programming},
PUBLISHER = {Prentice Hall},
YEAR = 1976
}
@MISC{euclid300bc,
AUTHOR = {Euclid},
TITLE = {Elements},
YEAR = {300B.C.},
URL = {http://www-groups.dcs.st-andrews.ac.uk/~history/Mathematicians/Euclid.html}
}
@BOOK{euclid1956,
AUTHOR = {Euclid},
TITLE = {Elements},
PUBLISHER = {Dover},
YEAR = 1956,
NOTE = {Translated by Sir Thomas L. Heath}
}
@ARTICLE{farmer1993,
AUTHOR = {William M. Farmer and Joshua D. Guttman and F. Javier Thayer},
TITLE = {{IMPS}: An Interactive Mathematical Proof System},
JOURNAL = {Journal of Automated Reasoning},
YEAR = 1993,
VOLUME = 11,
PAGES = {213--248},
URL = {http://imps.mcmaster.ca/wmfarmer/publications.html},
ABSTRACT = {IMPS is an Interactive Mathematical Proof System intended as a
general purpose tool for formulating and applying mathematics in a
familiar fashion. The logic of IMPS is based on a version of simple
type theory with partial functions and subtypes. Mathematical
specification and inference are performed relative to axiomatic
theories, which can be related to one another via inclusion and theory
interpretation. IMPS provides relatively large primitive inference
steps to facilitate human control of the deductive process and human
comprehension of the resulting proofs. An initial theory library
containing almost a thousand repeatable proofs covers significant
portions of logic, algebra and analysis, and provides some support for
modeling applications in computer science.}
}
@ARTICLE{feldman1984,
AUTHOR = {V. A. Feldman and D. Harel},
TITLE = {A probabilistic dynamic logic},
JOURNAL = {Journal of Computer and System Sciences},
VOLUME = {28},
NUMBER = {2},
PAGES = {193--215},
YEAR = 1984
}
@ARTICLE{fidge2003,
AUTHOR = {C. Fidge and C. Shankland},
TITLE = {But what if {I} don't want to wait forever?},
JOURNAL = {Formal Aspects of Computing},
YEAR = {to appear in 2003}
}
@BOOK{fishman1996,
AUTHOR = {George S. Fishman},
TITLE = {Monte Carlo: Concepts, Algorithms and Applications},
PUBLISHER = {Springer},
YEAR = 1996
}
@BOOK{fleuriot2001,
AUTHOR = {J. D. Fleuriot},
TITLE = {A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton's Principia},
PUBLISHER = {Springer},
SERIES = {Distinguished Dissertations},
YEAR = {2001}
}
@INPROCEEDINGS{gabbay1992,
AUTHOR = {Dov M. Gabbay and Hans J{\"u}rgen Ohlbach},
TITLE = {Quantifier elimination in second--order predicate logic},
BOOKTITLE = {Principles of Knowledge Representation and Reasoning (KR92)},
YEAR = 1992,
EDITOR = {Bernhard Nebel and Charles Rich and William Swartout},
PAGES = {425--435},
PUBLISHER = {Morgan Kaufmann},
URL = {http://www.pms.informatik.uni-muenchen.de/mitarbeiter/ohlbach/homepage/publications/PL/abstracts.shtml#scan},
ABSTRACT = {An algorithm is presented which eliminates second--order quantifiers
over predicate variables in formulae of type exists P1,...,PnF where F
is an arbitrary formula of first--order predicate logic. The resulting
formula is equivalent to the original formula -- if the algorithm
terminates. The algorithm can for example be applied to do
interpolation, to eliminate the second--order quantifiers in
circumscription, to compute the correlations between structures and
power structures, to compute semantic properties corresponding to
Hilbert axioms in non classical logics and to compute model theoretic
semantics for new logics.}
}
@MISC{gathercole1997,
AUTHOR = {Chris Gathercole and Peter Ross},
TITLE = {Small Populations over Many Generations can beat Large Populations over Few Generations in Genetic Programming},
HOWPUBLISHED = {http://www.dai.ed.ac.uk/students/chrisg/},
YEAR = 1997
}
@ARTICLE{gill1977,
AUTHOR = {J. T. Gill},
TITLE = {Computational complexity of probabilistic {Turing} machines},
JOURNAL = {SIAM Journal on Computing},
VOLUME = 6,
NUMBER = 4,
PAGES = {675--695},
MONTH = DEC,
YEAR = 1977,
ABSTRACT = {"This paper defines the basic notion of a probabilistic Turing machine
(PTM). A PTM computes a partial function that assigns to each input
the output which occurs with a probability greater than half. It is
shown that a NDTM can be simulated by a PTM in the same space but with
a small error probability. Gill also considers the complexity classes
RP, PP, and BPP for polynomial-time PTMs (see Section 4.1). He shows
that $\mbox{P} \subseteq \mbox{RP} \subseteq \mbox{BPP} \subseteq
\mbox{PP} \subseteq \mbox{PSPACE}$ and that $\mbox{RP} \subseteq
\mbox{NP} \subseteq \mbox{PP}$."}
}
@BOOK{girard1989,
AUTHOR = {Jean-Yves Girard},
SERIES = {Cambridge tracts in theoretical computer science},
SUBJECT = {Electronic digital computers--Programming Proof theory Type theory},
VOLUME = {7},
CAMLIB = {[Univ. Lib.] 348:8.b.95.262 South Front 4},
PUBLISHER = {Cambridge University Press},
PAGES = {xi,176p},
YEAR = 1989,
CITY = {Cambridge},
SIZE = {26cm},
TITLE = {Proofs and types}
}
@ARTICLE{godel1931,
AUTHOR = {K. G{\"o}del},
JOURNAL = {Monatshefte f{\"u}r Mathematik und Physik},
PAGES = {173--198},
TITLE = {{\"U}ber formal unentscheidbare {S}{\"a}tze der {P}rincipia {M}athematica und verwandter {S}ysteme},
VOLUME = 38,
YEAR = 1931
}
@BOOK{godel1962,
AUTHOR = {K. G{\"o}del},
TITLE = {On Formally Undecidable Propositions of Principia Mathematica and Related Systems},
YEAR = 1962,
PUBLISHER = {Oliver and Boyd},
NOTE = {Translated by B. Meltzer},
ADDRESS = {London}
}
@BOOK{goguen1996,
AUTHOR = {J. Goguen and G. Malcolm},
TITLE = {Algebraic Semantics of Imperative Programs},
EDITION = {1st},
PUBLISHER = {MIT Press},
ADDRESS = {Cambridge, Mass.},
YEAR = 1996,
ISBN = {0-262-07172-X}
}
@INPROCEEDINGS{goldberg2002,
AUTHOR = {E. Goldberg and Y. Novikov},
TITLE = {{BerkMin}: {A} Fast and Robust {SAT}-Solver},
BOOKTITLE = {Design, Automation, and Test in Europe (DATE '02)},
MONTH = MAR,
YEAR = 2002,
PAGES = {142--149},
URL = {http://www.ece.cmu.edu/~mvelev/goldberg_novikov_date02.pdf}
}
@BOOK{goldie1991,
AUTHOR = {Charles M. Goldie and Richard G. E. Pinch},
TITLE = {Communication theory},
SERIES = {LMS Student Texts},
VOLUME = 20,
PUBLISHER = {Cambridge University Press},
YEAR = 1991
}
@BOOK{gordon1979,
AUTHOR = {M. Gordon and R. Milner and C. Wadsworth},
TITLE = {Edinburgh {LCF}},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 78,
YEAR = 1979
}
@TECHREPORT{gordon1985,
AUTHOR = {Mike Gordon},
TITLE = {Why {H}igher-{O}rder {L}ogic is a Good Formalism For Specifying and Verifying Hardware},
YEAR = 1985,
INSTITUTION = {Computer Laboratory, The University of Cambridge},
NUMBER = 77
}
@BOOK{gordon1988,
AUTHOR = {M. J. C. Gordon},
TITLE = {Programming Language Theory and its Implementation},
PUBLISHER = {Prentice Hall},
YEAR = 1988
}
@INCOLLECTION{gordon1988a,
AUTHOR = {Michael J. C. Gordon},
TITLE = {{HOL}: A proof generating system for higher-order logic},
BOOKTITLE = {{VLSI} Specification, Verification and Synthesis},
EDITOR = {Graham Birtwistle and P. A. Subrahmanyam},
YEAR = 1988,
PAGES = {73--128},
PUBLISHER = {Kluwer Academic Publishers},
ADDRESS = {Boston}
}
@INCOLLECTION{gordon1989,
AUTHOR = {M. J. C. Gordon},
TITLE = {Mechanizing Programming Logics in Higher Order Logic},
BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Springer-Verlag},
YEAR = 1989,
PAGES = {387--439},
URL = {ftp://ftp.cl.cam.ac.uk/hvg/papers/Banffpaper.dvi.gz}
}
@BOOK{gordon1993,
EDITOR = {M. J. C. Gordon and T. F. Melham},
TITLE = {Introduction to HOL (A theorem-proving environment for higher order logic)},
PUBLISHER = {Cambridge University Press},
YEAR = 1993
}
@TECHREPORT{gordon1994,
AUTHOR = {Mike Gordon},
TITLE = {Merging {HOL} with Set Theory: preliminary experiments},
INSTITUTION = {University of Cambridge Computer Laboratory},
NUMBER = 353,
MONTH = NOV,
YEAR = 1994,
URL = {http://www.cl.cam.ac.uk/users/mjcg/papers/holst},
ABSTRACT = {Set theory is the standard foundation for mathematics, but the
majority of general purpose mechanized proof assistants support
versions of type theory (higher order logic). Examples include Alf,
Automath, Coq, Ehdm, HOL, IMPS, Lambda, LEGO, Nuprl, PVS and
Veritas. For many applications type theory works well and provides,
for specification, the benefits of type-checking that are well-known
in programming. However, there are areas where types get in the way or
seem unmotivated. Furthermore, most people with a scientific or
engineering background already know set theory, whereas type theory
may appear inaccessable and so be an obstacle to the uptake of proof
assistants based on it. This paper describes some experiments (using
HOL) in combining set theory and type theory; the aim is to get the
best of both worlds in a single system. Three approaches have been
tried, all based on an axiomatically specified type V of ZF-like sets:
(i) HOL is used without any additions besides V; (ii) an embedding of
the HOL logic into V is provided; (iii) HOL axiomatic theories are
automatically translated into set-theoretic definitional
theories. These approaches are illustrated with two examples: the
construction of lists and a simple lemma in group theory.}
}
@UNPUBLISHED{gordon1996,
AUTHOR = {M. J. C. Gordon},
TITLE = {Notes on {PVS} from a {HOL} perspective},
YEAR = 1996,
NOTE = {Available from the author's web page},
URL = {http://www.cl.cam.ac.uk/~mjcg/PVS.html},
ABSTRACT = {During the first week of July 1995 I visited SRI Menlo Park to find
out more about PVS (Prototype Verification System). The preceding week
I attended LICS95, where I had several talks with Natarajan Shankar
accompanied by demos of the system on his SparcBook laptop. This note
consists of a somewhat rambling and selective report on some of the
things I learned, together with a discussion of their implications for
the evolution of the HOL system.}
}
@ARTICLE{gordon2002,
AUTHOR = {Michael J. C. Gordon},
TITLE = {Programming combinations of deduction and {BDD}-based symbolic calculation},
JOURNAL = {LMS Journal of Computation and Mathematics},
VOLUME = 5,
PAGES = {56--76},
MONTH = AUG,
YEAR = 2002,
URL = {http://www.lms.ac.uk/jcm/5/lms2000-001},
ABSTRACT = {A generalisation of Milner's `LCF approach' is described. This allows
algorithms based on binary decision diagrams (BDDs) to be programmed
as derived proof rules in a calculus of representation judgements. The
derivation of representation judgements becomes an LCF-style proof by
defining an abstract type for judgements analogous to the LCF type of
theorems. The primitive inference rules for representation judgements
correspond to the operations provided by an efficient BDD package
coded in C (BuDDy). Proof can combine traditional inference with steps
inferring representation judgements. The resulting system provides a
platform to support a tight and principled integration of theorem
proving and model checking. The methods are illustrated by using them
to solve all instances of a generalised Missionaries and Cannibals
problem.}
}
@INPROCEEDINGS{gordon2003,
AUTHOR = {Mike Gordon and Joe Hurd and Konrad Slind},
TITLE = {Executing the formal semantics of the {Accellera} {Property} {Specification} {Language} by mechanised theorem proving},
BOOKTITLE = {Correct Hardware Design and Verification Methods},
PAGES = {200--215},
MONTH = OCT,
YEAR = 2003,
EDITOR = {Daniel Geist and Enrico Tronci},
VOLUME = 2860,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer},
URL = {http://www.cl.cam.ac.uk/users/jeh1004/research/papers/sugar.html},
ABSTRACT = {The Accellera Property Specification Language (PSL) is designed for
the formal specification of hardware. The Reference Manual contains a
formal semantics, which we previously encoded in a machine readable
version of higher order logic. In this paper we describe how to
`execute' the formal semantics using proof scripts coded in the HOL
theorem prover's metalanguage ML. The goal is to see if it is feasible
to implement useful tools that work directly from the official
semantics by mechanised proof. Such tools will have a high assurance
of conforming to the standard. We have implemented two experimental
tools: an interpreter that evaluates whether a finite trace $w$, which
may be generated by a simulator, satisfies a PSL formula $f$ (i.e.~$w
\models f$), and a compiler that converts PSL formulas to checkers in
an intermediate format suitable for translation to HDL for inclusion
in simulation test-benches. Although our tools use logical deduction
and are thus slower than hand-crafted implementations, they may be
speedy enough for some applications. They can also provide a reference
for more efficient implementations.}
}
@TECHREPORT{gunter1989,
AUTHOR = {Elsa Gunter},
TITLE = {Doing Algebra in Simple Type Theory},
YEAR = 1989,
INSTITUTION = {Department of Computer and Information Science, University of Pennsylvania},
NUMBER = {MS-CIS-89-38, Logic \&\ Computation 09}
}
@BOOK{hajek1998,
AUTHOR = {Petr H\'ajek},
TITLE = {Metamathematics of Fuzzy Logic},
MONTH = AUG,
YEAR = 1998,
SERIES = {Trends in Logic},
VOLUME = 4,
PUBLISHER = {Kluwer Academic Publishers},
ADDRESS = {Dordrecht},
URL = {http://www.wkap.nl/prod/b/0-7923-5238-6},
ABSTRACT = {This book presents a systestematic treatment of deductive aspects and
structures of fuzzy logic understood as many valued logic sui
generis. Some important systems of real-valued propositional and
predicate calculus are defined and investigated. The aim is to show
that fuzzy logic as a logic of imprecise (vague) propositions does
have well-developed formal foundations and that most things usually
named `fuzzy inference' can be naturally understood as logical
deduction.
There are two main groups of intended readers. First, logicians: they
can see that fuzzy logic is indeed a branch of logic and may find
several very interesting open problems. Second, equally important,
researchers involved in fuzzy logic applications and soft
computing. As a matter of fact, most of these are not professional
logicians so that it can easily happen that an application, clever and
successful as it may be, is presented in a way which is logically not
entirely correct or may appear simple-minded. (Standard presentations
of the logical aspects of fuzzy controllers are the most typical
example.) This fact would not be very important if only the bon ton of
logicians were harmed; but it is the opinion of the author (who is a
mathematical logician) that a better understanding of the strictly
logical basis of fuzzy logic (in the usual broad sense) is very useful
for fuzzy logic appliers since if they know better what they are
doing, they may hope to do it better. In addition, a better mutual
understanding between (classical) logicians and researchers in fuzzy
logic, promises to lead to deeper cooperation and new results.
Audience: mathematicians, logicians, computer scientists, specialists
in artificial intelligence and knowledge engineering, developers of
fuzzy logic.}
}
@ARTICLE{halpern1990,
AUTHOR = {Joseph Y. Halpern},
TITLE = {An analysis of first-order logics of probability},
JOURNAL = {Artificial Intelligence},
YEAR = 1990,
URL = {http://www.cs.cornell.edu/home/halpern/abstract.html#journal25},
ABSTRACT = {We consider two approaches to giving semantics to first-order logics
of probability. The first approach puts a probability on the domain,
and is appropriate for giving semantics to formulas involving
statistical information such as ``The probability that a randomly
chosen bird flies is greater than .9.'' The second approach puts a
probability on possible worlds, and is appropriate for giving
semantics to formulas describing degrees of belief, such as ``The
probability that Tweety (a particular bird) flies is greater than
.9.'' We show that the two approaches can be easily combined, allowing
us to reason in a straightforward way about statistical information
and degrees of belief. We then consider axiomatizing these logics. In
general, it can be shown that no complete axiomatization is
possible. We provide axiom systems that are sound and complete in