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

Proofs.InferBasic

Description

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

Documentation

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

applies basic inference to a given node. The result is a theory which is either a model after a consistency check or a new theory for the node label