Contents of Report

[Data of Report]

Report Number:
TR0642
Date of Registration:
1991.05
English Title:
A Collection of Logical System and Proofs Implemented in EUODHILOS I
Japanese Title:
***
English Author:
H.Sawamura,T.Minami,T.Ohtani,K.Yokota,K.Ohashi
Japanese:
***
Name of Organization to which author belongs:
Fujitsu,Fujitsu,Fujitsu,Fujitsu,Fujitsu
PDF:
tr0642.pdf

[Contents]

Abstract.... 3
1Introduction.... 6
2First-Order logic(NK).... 8
2.1Language system of First-Order logic.... 8
2.2Derivation system of First-Order logic.... 9
2.3Unsolvability proof of the halting problem.... 9
3Constructive Type Theory.... 11
3.1Language system of Constructive Type Theory.... 11
3.2Derivation system of Constructive Type Theory.... 13
3.3Proof Examples.... 15
4Hoare logic.... 18
4.1Language system of Hoare logic.... 18
4.2Derivation system of Hoare logic.... 19
4.3Partial correctness proof of a program.... 19
5Dynamic Logic.... 21
5.1Language system of Dynamic Logic.... 21
5.2Derivation system of Dynamic Logic.... 22
5.3Reasoning about Programs.... 24
6Intensional logic.... 25
6.1Language system of Intensional logic.... 25
6.2Derivation system of Intensional logic.... 26
6.3Reflective proof and Montague's semantics.... 27
7General logic.... 29
7.1Language system of General logic.... 29
7.2Derivation system of General logic.... 30
7.3Proof Examples.... 32
8Relevance logic-Implecational calculus R based on tag calculus.... 34
8.1Language system of R.... 34
8.2Derivation system of R.... 34
8.3Proof Examples.... 35
9Category Theory.... 37
9.1Language system of Category Theory.... 37
9.2Derivation system of Category Theory.... 38
9.3Derived rules.... 40
9.4Proof Examples.... 41
10Miscellany.... 43
10.1Smullyan's logical Puzzles.... 43
10.2Propositional Modal logic(T).... 43
10.3Second-Order reasoning.... 43
10.4Proof by Structual induction on list.... 46
Acknowledgements.... 47
References.... 47
End.... 48

目次をクリックすると、PDFファイルが表示されます。

ICOT研究論文（TR）一覧に戻る / Back to the list of ICOT Technical Reports