\contentsline {section}{\numberline {1}Introduction}{2}
\contentsline {section}{\numberline {2}The Language: Parsing, Display, Declarations}{4}
\contentsline {subsection}{\numberline {2.1}Tokens}{4}
\contentsline {subsection}{\numberline {2.2}Syntax}{7}
\contentsline {section}{\numberline {3}Set Theory and Defined Notions}{9}
\contentsline {subsection}{\numberline {3.1}The Stratification Algorithm}{11}
\contentsline {section}{\numberline {4}Proof Trees and The Logic of Propositions}{12}
\contentsline {subsection}{\numberline {4.1}Sequents}{12}
\contentsline {subsection}{\numberline {4.2}Proof Trees}{14}
\contentsline {subsection}{\numberline {4.3}Sequent Rules in General}{16}
\contentsline {subsection}{\numberline {4.4}Specific Sequent Rules: Connectives}{16}
\contentsline {subsection}{\numberline {4.5}Axiom}{17}
\contentsline {subsection}{\numberline {4.6}Left rules}{17}
\contentsline {subsection}{\numberline {4.7}Right rules}{17}
\contentsline {section}{\numberline {5}Variables and Substitution}{18}
\contentsline {section}{\numberline {6}More Sequent Rules}{19}
\contentsline {subsection}{\numberline {6.1}Rules for Quantifiers}{19}
\contentsline {subsubsection}{\numberline {6.1.1}Left Rules}{19}
\contentsline {subsubsection}{\numberline {6.1.2}Right Rules}{20}
\contentsline {subsubsection}{\numberline {6.1.3}Comments on Quantifier Rules}{20}
\contentsline {subsection}{\numberline {6.2}Rules for Membership}{20}
\contentsline {subsubsection}{\numberline {6.2.1}Left Rule}{20}
\contentsline {subsubsection}{\numberline {6.2.2}Right Rule}{20}
\contentsline {subsection}{\numberline {6.3}Rules for Equality}{21}
\contentsline {subsubsection}{\numberline {6.3.1}Left Rule}{21}
\contentsline {subsubsection}{\numberline {6.3.2}Right Rule}{21}
\contentsline {subsubsection}{\numberline {6.3.3}Comments on Equality Rules}{21}
\contentsline {subsection}{\numberline {6.4}Global Substitution, manual and automatic}{21}
\contentsline {section}{\numberline {7}Proving and Using Theorems}{22}
\contentsline {section}{\numberline {8}Cut and ``Theorem Cut''}{22}
\contentsline {section}{\numberline {9}The Theorem List and Reading Saved Proofs}{23}
\contentsline {section}{\numberline {10}Alternative Logics}{23}
\contentsline {section}{\numberline {11}Future Developments}{24}
\contentsline {section}{\numberline {12}Examples of Use of Marcel}{24}
\contentsline {section}{\numberline {13}Command Reference}{36}
\contentsline {subsection}{\numberline {13.1}Commands Listed Alphabetically}{36}
\contentsline {subsection}{\numberline {13.2}Commands in Categories by Function}{44}
\contentsline {subsubsection}{\numberline {13.2.1}Prover Settings}{44}
\contentsline {subsubsection}{\numberline {13.2.2}Declaring Primitives and Syntax}{44}
\contentsline {subsubsection}{\numberline {13.2.3}Axioms, Definitions, and Theorems}{46}
\contentsline {subsubsection}{\numberline {13.2.4}Proof Manipulations}{47}
\contentsline {subsubsection}{\numberline {13.2.5}Starting and Finishing Sequents}{48}
\contentsline {subsubsection}{\numberline {13.2.6}Sequent Manipulations}{49}
\contentsline {subsubsection}{\numberline {13.2.7}Lists and Displays}{51}
\contentsline {subsubsection}{\numberline {13.2.8}History}{52}
\contentsline {subsubsection}{\numberline {13.2.9}Loading and Saving}{53}