Back to: Automated reasoning UNB Computer Science UNB
 MARMOSET Marmoset Automated Reasoner Mostly Only Solves Easy Theorems

M.A.R.M.O.S.E.T. stands for Marmoset Automated Reasoner Mostly Only Solves Easy Theorems. We hope this acronym is an adequate reflection of our humility, rather than our expectations. The hopes we have for Marmoset are the accurate and sound implementations of various algorithms that have, to our knowledge, not been implemented in any theorem prover.

With this theorem prover as a baseline for our experiments, we hope to provide empirical evidence to support the usage, dismissal, or further discussion and evolution of our ideas.

It is also expected that the implementation of the various algorithms in a sufficiently robust and fast language, in our case C++, will make Marmoset quite the stud (competitive). The competition we are most interested in is the CASC-17 competition (2000).

 
Algorithms
  

A-ordering is one of the more common ordering techniques used in several current competitive theorem provers. The alternative we are considering is Rank Activity, which has thus far not been implemented for empirical testing. Details will follow, with time.

Minimal Binary Resolution Trees (BRT) according to Spencer-Horton's clause tree definition eliminate equivalent proof trees. The use of minimal clause trees via the surgery algorithm will eliminate the redundant non-minimal proofs. This may save much memory and reduce the running time of the theorem prover. We are unaware of the overall effects of surgery, but intend to conduct empirical studies of proof generation with and without surgery.

Implementation Specific

  • Page oriented memory manager, to avoid the overhead of operating system memory managers.
  • Data structures: hash table, stack, queue.

Algorithms that have not yet been finalized (should they be used):

  • Clause subsumption (Forward, backward)
  • Unification
  • Equality (preprocessed)
 
Compilation
  

Marmoset compiles under the following (at least):
  • Solaris 2.6 GNU C/C++ 2.8.1 (-O1 optimizations only) on UltraSparc
  • Microsoft Visual C++ v6.0 on Windows 95/98/NT
  • DJGPP on MS-DOS

Marmoset classes are being documented with hdoc. The documentation, when available, will be found at http://www.unb.ca/research_areas/ar/marmoset.html

This page maintained by Brian M. Hunt

 
... so under construction it's still in the emacs buffer ...