Satisfiability Calculus: An Abstract Formulation of Semantic Proof Systems

What is it about?

The main contribution of this paper is the definition of Satisfiability Calculus as a semantic counterpart of Proof Calculus in the context of algebraic specification as introduced by Joseph Goguen and Rod Burstall and deeply studied by José Meseguer in his work General Logics.

Featured Image

Why is it important?

The contribution of this paper, in some way, completes the landscape of formal structures used in algebraic specification to characterize the different aspects of a logical system by introducing a general formalization of procedures aiming at model construction; thus, proving theoretical foundations to tools used in computer science such as model checkers.