Appendices for automated theorem proving in Euler diagram systems

Gem Stapleton, J. Masthoff, J. Flower, Andrew Fish, J. Southern

Research output: Other contributionResearch

Abstract

This report is a series of appendices to accompany the paper Automated Theorem Proving in Euler Diagram Systems. Here we include some details omitted from that paper and some additional discussions that may be of interest. In appendix A, we give an overview of the A* search algorithm in the context of theorem proving. We establish the expressiveness of Euler diagrams in appendix B. A complete worked example showing how to calculate the restrictive heuristic is given in appendix C. The proofs of the three theorems given in the paper are included in appendix D. The notion of clutter in Euler diagrams and how our tactics steer Edith towards proofs containing diagrams with low `clutter scores' is covered in appendix E. Details on how we generated proof tasks to evaluate Edith are given in appendix F. Finally, much of our evaluation is presented in appendix G, although the main results are included in the paper.
Original languageEnglish
PublisherUniversity of Brighton
Number of pages35
Place of PublicationBrighton, UK
Publication statusPublished - 2006

Fingerprint

Automated Theorem Proving
Euler
Diagram
Clutter
Theorem Proving
Expressiveness
Search Algorithm
Heuristics
Calculate
Series
Evaluate
Evaluation
Theorem

Bibliographical note

VMG.06.2

Cite this

Stapleton, G., Masthoff, J., Flower, J., Fish, A., & Southern, J. (2006). Appendices for automated theorem proving in Euler diagram systems. Brighton, UK: University of Brighton.
Stapleton, Gem ; Masthoff, J. ; Flower, J. ; Fish, Andrew ; Southern, J. / Appendices for automated theorem proving in Euler diagram systems. 2006. Brighton, UK : University of Brighton. 35 p.
@misc{caf980ac51c64dbb947abd84e1ab6dc9,
title = "Appendices for automated theorem proving in Euler diagram systems",
abstract = "This report is a series of appendices to accompany the paper Automated Theorem Proving in Euler Diagram Systems. Here we include some details omitted from that paper and some additional discussions that may be of interest. In appendix A, we give an overview of the A* search algorithm in the context of theorem proving. We establish the expressiveness of Euler diagrams in appendix B. A complete worked example showing how to calculate the restrictive heuristic is given in appendix C. The proofs of the three theorems given in the paper are included in appendix D. The notion of clutter in Euler diagrams and how our tactics steer Edith towards proofs containing diagrams with low `clutter scores' is covered in appendix E. Details on how we generated proof tasks to evaluate Edith are given in appendix F. Finally, much of our evaluation is presented in appendix G, although the main results are included in the paper.",
author = "Gem Stapleton and J. Masthoff and J. Flower and Andrew Fish and J. Southern",
note = "VMG.06.2",
year = "2006",
language = "English",
publisher = "University of Brighton",
type = "Other",

}

Stapleton, G, Masthoff, J, Flower, J, Fish, A & Southern, J 2006, Appendices for automated theorem proving in Euler diagram systems. University of Brighton, Brighton, UK.

Appendices for automated theorem proving in Euler diagram systems. / Stapleton, Gem; Masthoff, J.; Flower, J.; Fish, Andrew; Southern, J.

35 p. Brighton, UK : University of Brighton. 2006, .

Research output: Other contributionResearch

TY - GEN

T1 - Appendices for automated theorem proving in Euler diagram systems

AU - Stapleton, Gem

AU - Masthoff, J.

AU - Flower, J.

AU - Fish, Andrew

AU - Southern, J.

N1 - VMG.06.2

PY - 2006

Y1 - 2006

N2 - This report is a series of appendices to accompany the paper Automated Theorem Proving in Euler Diagram Systems. Here we include some details omitted from that paper and some additional discussions that may be of interest. In appendix A, we give an overview of the A* search algorithm in the context of theorem proving. We establish the expressiveness of Euler diagrams in appendix B. A complete worked example showing how to calculate the restrictive heuristic is given in appendix C. The proofs of the three theorems given in the paper are included in appendix D. The notion of clutter in Euler diagrams and how our tactics steer Edith towards proofs containing diagrams with low `clutter scores' is covered in appendix E. Details on how we generated proof tasks to evaluate Edith are given in appendix F. Finally, much of our evaluation is presented in appendix G, although the main results are included in the paper.

AB - This report is a series of appendices to accompany the paper Automated Theorem Proving in Euler Diagram Systems. Here we include some details omitted from that paper and some additional discussions that may be of interest. In appendix A, we give an overview of the A* search algorithm in the context of theorem proving. We establish the expressiveness of Euler diagrams in appendix B. A complete worked example showing how to calculate the restrictive heuristic is given in appendix C. The proofs of the three theorems given in the paper are included in appendix D. The notion of clutter in Euler diagrams and how our tactics steer Edith towards proofs containing diagrams with low `clutter scores' is covered in appendix E. Details on how we generated proof tasks to evaluate Edith are given in appendix F. Finally, much of our evaluation is presented in appendix G, although the main results are included in the paper.

M3 - Other contribution

PB - University of Brighton

CY - Brighton, UK

ER -

Stapleton G, Masthoff J, Flower J, Fish A, Southern J. Appendices for automated theorem proving in Euler diagram systems. 2006. 35 p.