12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 14:36, 27 August 2009
, 14:36, 27 August 2009→Case analysis-synthesis theorem: convert graphics
Some of the jobs that the CAST can be usefully put to work on are proving propositional theorems and establishing equations between propositions. Once again, let us turn to the example of Leibniz's ''Praeclarum Theorema'' as a way of illustrating how.
Some of the jobs that the CAST can be usefully put to work on are proving propositional theorems and establishing equations between propositions. Once again, let us turn to the example of Leibniz's ''Praeclarum Theorema'' as a way of illustrating how.
{| align="center" cellpadding="10" style="text-align:center; width:90%"
{| align="center" cellpadding="8"
|
|
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
|-
| Praeclarum Theorema. Proof by CAST. |
| [[Image:Proof Praeclarum Theorema CAST 00.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 01.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast A.jpg|500px]]
| a o o d o ad |
|-
| [[Image:Proof Praeclarum Theorema CAST 02.jpg|500px]]
|-
| | |
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 03.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| bc |
| [[Image:Proof Praeclarum Theorema CAST 04.jpg|500px]]
|-
| | | | | | |/ |
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| \ / | \ / | |
| [[Image:Proof Praeclarum Theorema CAST 05.jpg|500px]]
|-
| | | |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
| | | |
|-
| a o-----------------------------o---o a |
| [[Image:Proof Praeclarum Theorema CAST 06.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast D.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 07.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 08.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 09.jpg|500px]]
| b o o c o bc o c o |
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| \ / | \ / | |
| [[Image:Proof Praeclarum Theorema CAST 10.jpg|500px]]
| o-------o o-------o |
|-
| | | |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 11.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cast B.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 12.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 13.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Domination.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 14.jpg|500px]]
| b o o c o bc o c |
|-
| | | | | |
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 15.jpg|500px]]
| o-------o o-------o |
|-
| [[Image:Equational Inference Bar -- Cast C.jpg|500px]]
|-
| a o-----------------------------o---o a |
| [[Image:Proof Praeclarum Theorema CAST 16.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 17.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- Cancellation.jpg|500px]]
|-
| [[Image:Proof Praeclarum Theorema CAST 18.jpg|500px]]
|-
| [[Image:Equational Inference Bar -- QED.jpg|500px]]
|}
| b o o c o bc |
| | | | |
| o o d o d |
| | | |
| b o o c o bc |
| | | | |
| o o d o d |
| \ / | |
| a o-----------------------------o---o a |
| \ / |
| \ / | \ / | |
| \ / |
| b |
| | | |
| | | |
| \ / |
| \ / | \ |
| | | |
| | | |
| \ / |
| b o o c o bc |
| | | |
| | | |
| \ / |
| b o o c o bc |
| | | | |
| o-------o |
| | |
| \ / |
| \ / |
| \ / |
| \ / |
| o c o c o c o c |
| | | |
| \ / |
| \ / |
| o-------o o |
| | | |
| | | |
| a o---o---o a |
| o c o c |
| | |
| b o-------------------------o---o b |
| d o---o---o d |
| a o---o---o a |
| \ / |
| | | | | |
| c o-------------------------o---o c |
| o-------o o-------o |
| | | |
| c o-------------------------o---o c |
| \ / |
| c o---o---o c |
| \ / |
| b o---o---o b |
| d o---o---o d |
| \ / |
| (23)
| (23)
|}
|}