Seqs

This page is about Seqs, a unification-aided theorem prover for the intuitionistic sequent calculus.

Introduction

Seqs—a punny name short for "sequents"—is an O'Caml implementation of Daniel Leivant's note "An Alternative Way of Using Unification in Proof-Search". It uses the standard constructive sequent calculus inference rules, except for the "non-terminating" left universal rule: Rather than repeatedly instantiating universals with concrete terms, "term namers" (i.e., fresh logic variables) are used when "forcing" a universal. A set of constraints ensures that these variables are used only in the right ways (i.e., respecting variable scopes), and these constraints are resolved by a separate unification step when a proof branch is closed.

Seqs was originally created as my final project for Prof. Leivant's Automated Deduction course, autumn 2005. I have tested it with O'Caml 3.08.4; use any other version at your own risk. Seqs is a prototype, and has had absolutely no work done on efficiency or other optimisations; it is slow. Seqs is released under the terms of the GPL.

News

• 2005-12-16–uploaded the first release

Download

• Seqs is open-source; the only available download is the O'Caml source:
• some example proofs produced by Seqs:
  • examples (txt)

Screenshot

Seqs in action, starting up and running through a simple proof.

More Information

Well, there's really no more information available for the time being, sorry! Please check back soon, though, or e-mail me if you have specific questions.