Contents of Report

[Data of Report]

	Abstract	.... 2
	Contents	.... 3
1	Introduction	.... 5
2	Getting Started	.... 7
2.1	Starting EUODHILOS	.... 7
2.2	Creating a new Logic	.... 9
2.3	Closing EUODHILOS	.... 9
2.4	Manipulating a Logic	.... 9
2.5	Functions Menu of a Logic	.... 10
2.6	Defining Syntax	.... 11
2.7	Defining Inference Rules	.... 13
2.8	Proving on a Sheet of Thought	.... 18
3	Overview of EUODHILOS	.... 26
4	Creating a Logic	.... 27
5	Special Symbols	.... 29
6	Syntax Description	.... 32
6.1	Syntax Editor	.... 32
6.2	Extended DCG part	.... 34
6.3	Constructor declaration	.... 35
6.4	Remarks on Syntax Description	.... 36
7	Inference and Rewriting Rules	.... 37
7.1	Opening and Closing an Inference Rule Menu	.... 37
7.2	Defining and Modifying an Inference	.... 38
7.3	Side Conditions	.... 39
7.4	Rewriting Rules	.... 40
8	Axioms	.... 40
9	Proof Construction on a Sheet of Thought	.... 42
9.1	Assumption	.... 45
9.2	Derivation	.... 46
9.3	Metavariables	.... 52
9.4	Editing Proof Fragments	.... 55
9.5	Other Facilities of Sheet of Thought	.... 60
	Acknowledgement	.... 64
	References	.... 64
A	Appendix	.... 66
A.1	First-order Logic	.... 66
A.2	Category Theory	.... 67
A.3	Hoare Logic	.... 68
A.4	Relevant Logic	.... 69
	End	.... 73

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