Copyright | (c) J. Gerken T. Mossakowski K. Luettich Uni Bremen 2002-2006 |
---|---|

License | GPLv2 or higher, see LICENSE.txt |

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

Stability | provisional |

Portability | non-portable(Logic) |

Safe Haskell | None |

devGraph rule that calls provers for specific logics

Proof rule "basic inference" in the development graphs calculus. Follows Sect. IV:4.4 of the CASL Reference Manual.

References:

T. Mossakowski, S. Autexier and D. Hutter: Extending Development Graphs With Hiding. H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001, Lecture Notes in Computer Science 2029, p. 269-283, Springer-Verlag 2001.

## Synopsis

- basicInferenceNode :: LogicGraph -> LibName -> DGraph -> LNode DGNodeLab -> LibEnv -> IORef IntState -> IO (Result G_theory)