Copyright | (c) Thiemo Wiedemeyer, Uni Bremen 2009 |
---|---|

License | GPLv2 or higher, see LICENSE.txt |

Maintainer | raider@informatik.uni-bremen.de |

Stability | provisional |

Portability | needs POSIX |

Safe Haskell | None |

Generic Gtk GUI for automatic theorem provers.

# Documentation

:: (Ord proof_tree, Ord sentence) | |

=> ATPFunctions sign sentence mor proof_tree pst | prover specific functions |

-> Bool | prover supports extra options |

-> String | prover name |

-> String | theory name |

-> Theory sign sentence proof_tree | theory consisting of a signature and a list of Named sentence |

-> [FreeDefMorphism sentence mor] | freeness constraints |

-> proof_tree | initial empty proof_tree |

-> IO [ProofStatus proof_tree] | proof status for each goal |