Added the trait at.logic.provers.Prover which supplies methods for proving, and checking validity of, sequents and formulas. Some 
implementations have been added as a glue to existing prover code (Prover9, MiniSAT, built-in LK proof-search).

The implementation of the Prover9 Prover object is not complete yet - construction of the proper LKProof objects is still missing.

Abstracted the cut-introduction code to make use of this trait. I have exposed this more general code to the CLI, but have not added 
documentation for it yet since presumably we don't want users to construct their own prover objects (but rather call some methods which 
construct pre-defined provers).


Please consider the following example CLI-run for more details.

// --------------------------------------------------------------

:load ../examples/ProofSequences.scala

val p = LinearEqExampleProof(4)

// --------------------------------------------------------------

// Use default prover: MiniSAT for validity check,
// built in LK proof-search for proof construction.
// Always works, but no support for equality.
cutIntroExp(p)

// --------------------------------------------------------------

// Use prover9. Will fail at proof construction since
// this is not supported (yet!). Once this is implemented, this
// should be used to apply CutIntro with equality support.
val prover = new at.logic.provers.prover9.Prover9Prover()
cutIntroExp(p, prover)

// --------------------------------------------------------------

// Use custom prover: Prover9 for validity check,
// built in LK proof-search for proof construction.
// Will fail at proof construction if Prover9 uses paramodulation.

val prover = new at.logic.provers.Prover() {
  def getLKProof( seq : FSequent ) =
    new at.logic.algorithms.lk.LKProver().getLKProof(seq)
  override def isValid( seq : FSequent ) = 
    new at.logic.provers.prover9.Prover9Prover().isValid(seq)
}

cutIntroExp(p, prover)

// --------------------------------------------------------------

// Use MiniSAT. Will fail at proof construction
// since MiniSAT does not support that.
val prover = new at.logic.provers.minisat.MiniSATProver()
cutIntroExp(p, prover)

// --------------------------------------------------------------

// Use built-in LK proof-search for both validity and
// proof construction. Will be slow.
val prover = new at.logic.algorithms.lk.LKProver()
cutIntroExp(p, prover)




git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1729 85d21ef8-add0-11de-ae77-5bfb9c5a3f34