- 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.