DIRECTORY OF THEORY FILES

• algebra2.wat working theory of reals/rationals in omnibus
• babydocs.wat examples from documentation
• capsl_capstuff.wat Shankar's belief logic proofs
• capsl_defination_file.wat
• capsl_ns_axioms.wat
• capsl_nsprotocol.wat
• capsl_svo.wat
• cohen*.wat A development from Cohen's book.
• combinators.wat Theoretical work on combinatory logic, with an eye to strong beta-reduction for Jonathan Seldin
• concepts.wat file intended to implement sequent proofs in the calculus of concepts
• counting.wat set theory under development using deduction.wat; includes proof of Schroder-Bernstein theorem.
• deduction.wat goal directed natural deduction prover using INPUT command candidate for addition to omnibus
• deduction_examples.wat examples (so far just one) for deduction.wat
• definitions.wat "structural" file for Math 387 development.
• examples.wat propositional logic examples for the Math 387 development.
• fract.wat Theory of rationals and reals continued in omnibus
• gries9.wat advanced logic in omnibus (quantifiers)
• jonny.wat calculator for working with exponents -- for Jonny uses peano
• lab3.wat part of the math 387 development.
• lambda.wat structural stuff in addition to structural.wat (in omnibus); includes the tactic for putting in explicit binders.
• life.wat a development of the theory of Conway's Game of Life.
• logic_tools.wat some logical stuff in omnibus; its leading comment follows: (* this file includes a selection of logical tools: Parvin tactics for conversion of "implication" theorems from one form to another, Alves-Foss theorems about case expressions, and basic results about quantifiers proved "by hand" *)
• logicdefs.wat basic logic definitions in omnibus l
• logicdefs2.wat Parvin's logic file -- propositional logic in omnibus
• mwu_subtraction.wat Minglong's proofs on subtraction and division.
• natorder.wat Sol's file on order on natural numbers, in omnibus
• new.quantifiers.wat theorems about quantifiers in omnibus
• newlib1.wat New library structural tactics.
• newlib2.wat New library equational development of propositional logic, independent of Watson logic of case expressions, followed by a development of INPUT driven sequent logic tactics for full first-order logic.
• newlib3.wat Chapter 1 of Landau (uses newlib1 and newlib2). This is Landau's theory of natural numbers.
• omnibus.wat The omnibus theory of almost everything
• pair_assign.wat Very complex theory of pair assignment operator from Minglong.
• peano.wat Peano arithmetic -- a laboratory for induction proofs. Not included in omnibus -- notationally incompatible with it, but complete induction and related results are exported from it to algebra2.wat in omnibus. theory of programming
• programs.wat implementing Cohen -- last file in omnibus theory.
• prop_equational.wat Is this part of the Math 387 development?
• prop_logic.wat Alternative version of logicdefs2 (Parvin's file) in something like its original form with propositional connectives as primitives; needed for belief logic.
• schneiderexample.wat Example of implementation of a type of syntactical objects.
• sequent.wat Development of sequent calculus in omnibus.
• shankar.wat A file on Shankar's capsl stuff -- I don't know whether it is older or newer than capsl* so I saved it.
• sharondemo.wat A demo.
• shortsheffer.wat Records a nice Boolean algebra result from the OTTER people (no proof!)
• simplesets.wat Sol's basic set theory in omnibus.
• sol_exp.wat Stuff about exponents developed by Sol to be added to omnibus eventually.
• structural.wat Basic structural tactics used by omnibus and most other files.
• struct2.wat file which updates things defined in structural.wat and lambda.wat to take advantage of new capabilities of the prover.
• tableau.wat develops the tautology checker NEWTAUT and proves the Gries axioms used in logicdefs2; in omnibus.
• tableau2.wat Simulation of a tableau style of reasoning in omnibus.
• typestuff.wat Basic stuff about types (retractions onto s.c. sets) in omnibus and other files.