next up previous contents
Next: Setting the Theory Filename Up: Theories Previous: Theories

Creating a new theory

We describe how to create your own theory.

Scroll the library window to the bottom of the library, and if you haven't already done so, add in delimiters for your own theory. Enter:





\begin{parbox} {25em} {\tt bottom ()\hspace{.2em}\lower.2ex\hbox{ \framebox {\r... ... \framebox {\rule[-.2ex]{0em}{1.5ex}\sc return} }\hspace{.2em}\ \\ }\end{parbox}




After the add_theory_delimiters function is evaluated, theory delimiters appear at the new bottom objects in the library window:

Library
*C class_prop_begin *********** CLASS PROP ****************
*t dneg_elim $\forall$A:${\Bbb{P}}${i}. $\neg$$\neg$A $\Rightarrow$A
*t imp_elim $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. (A $\Rightarrow$ B) $\Rightarrow$ $\neg$A $\vee$ B
*t neg_imp_elim $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. $\neg$(A $\Rightarrow$ B) $\Rightarrow$ A $\wedge$ $\neg$B
*t neg_or_elim $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. $\neg$(A $\vee$ B) $\Rightarrow$ $\neg$A $\wedge$ $\neg$B
*t neg_and_elim $\forall$A:${\Bbb{P}}${i}. $\forall$B:${\Bbb{P}}${i}. $\neg$(A $\wedge$ B) $\Rightarrow$ $\neg$A $\vee$ $\neg$B
*t pierce $\forall$P:${\Bbb{P}}${i}. $\forall$Q:${\Bbb{P}}${i}. ((P $\Rightarrow$ Q) $\Rightarrow$ P) $\Rightarrow$ P
*C class_prop_end ***************************************
*C user_begin ************** USER *****************
*C user_end *************************************
 
next up previous contents
Next: Setting the Theory Filename Up: Theories Previous: Theories
Dora Abdullah, 12/4/97