Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Fundamenta Informaticae

1 2019

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: institution theory

Sortuj według:

Ogranicz wyniki do:

Satisfiability Calculus : An Abstract Formulation of Semantic Proof Systems

Lopez Pombo Carlos G., Castro Pablo F., Aguirre Nazareno M., Maibaum Thomas S. E.

Fundamenta Informaticae

2019

Vol. 166, nr 4

297--347

The theory of institutions, introduced by Goguen and Burstall in 1984, can be thought of as an abstract formulation of model theory. This theory has been shown to be particularly useful in computer science, as a mathematical foundation for formal approaches to software construction. Institution theory was extended by a number of researchers, José Meseguer among them, who, in 1989, presented General Logics , wherein the model theoretical view of institutions is complemented by providing (categorical) structures supporting the proof theory of any given logic. In other words, Meseguer introduced the notion of proof calculus as a formalisation of syntactical deduction, thus “implementing” the entailment relation of a given logic. In this paper we follow the approach initiated by Goguen and introduce the concept of Satisfiability Calculus. This concept can be regarded as the semantical counterpart of Meseguer’s notion of proof calculus, as it provides the formal foundations for those proof systems that resort to model construction techniques to prove or disprove a given formula, thus “implementing” the satisfiability relation of an institution. These kinds of semantic proof methods have gained a great amount of interest in computer science over the years, as they provide the basic means for many automated theorem proving techniques.