net.sourceforge.czt.rules.prover

Interface Prover

All Known Implementing Classes:

SimpleProver

public interface Prover

A prover can be used to find proofs.

Different provers might use different strategies to find proofs (for example depth-first versus breadth-first search).

This very first version does not support searching for alternative proofs, nor does it support undos (reseting the bindings after a proof has been found). This needs updating!

Author:

Petra Malik

Method Summary

Modifier and Type	Method and Description
boolean	prove(net.sourceforge.czt.zpatt.ast.Sequent conclusion) Proves a given sequent.

Method Detail

prove

boolean prove(net.sourceforge.czt.zpatt.ast.Sequent conclusion)

Proves a given sequent. Returns true if a proof has been found. In this case, the Deduction element of the given Sequent contains the proof.