owards a Formula- tion of the Modularization Theorem for Presentations in Default Logics

CASSANO, VALENTÍN; LOPEZ POMBO, CARLOS GUSTAVO; MAIBAUM, THOMAS S. E.

Gregynog, Wales

Workshop; Workshop on Algebraic Development Techniques; 2016

Swansea, University

With an origin in Reiter?s seminal 1980 paper ?A Logic for Default Reasoning? (see [1]), default logics (DLs for short) are a sub-family of the log- ical approaches to nonmonotonic reasoning. DLs have received a great deal of attention and have accomplished much from the perspective of the study of non- monotonic consequence (see [2]). In comparison, with some noteworthy excep- tions (see [3,4,5,6]), the same cannot be said about the study of presentations of theories in DLs (default presentations for short) and of morphisms of said presentations (concepts analogous to those of algebraic specifications in classical logical systems). The latter opens an interesting niche for research if, light of the classics [7,8,9,10,11], we wish to design and construct default presentations that are not indivisible wholes but that result from ?putting together? default presentations that are more tractable and easier to understand. Intending to ful- fill this desideratum, we explore a formulation of default presentations, of their semantics, and of morphisms of default presentations. What we have in mind is the presentation of conditions that guarantee the existence of morphisms of default presentations, and a formulation and proof of a version of the so-called Modularization Theorem of [10,12] for default presentations. The use of DLs for reasoning about requirements (see [13]) provides an interesting area of applica- tion for our research efforts. We briefly explain our main ideas below.The Modularization Theorem was first presented in [14] as the main result of an investigation into the conditions that need to be added to an entailment relation to support an account of specification, where specifications are viewed as presentations of theories over the entailment relation. These ideas were worked out in detail in [10] and [12] for specifications in First-Order Logic (FOL for short) and extended to specifications in general logical systems later on in [15].The Modularization Theorem is interesting and relevant in the world of for- mal specifications because it is a basic tool for guaranteeing the preservation of modular structure in the stepwise development of specifications (see [10,12]). Borrowing an example from [12], in FOL, consider a situation in which: (i) a presentation ⟨Σ3, Φ3⟩ is a conservative extension of a presentation ⟨Σ1, Φ1⟩, indicated as ⟨Σ1, Φ1⟩ → ⟨Σ3, Φ3⟩, and (ii) a presentation ⟨Σ2, Φ2⟩ is an interpretation of ⟨Σ1,Φ1⟩ along a morphism m : Σ1 →Σ2 of signatures, indicated mas ⟨Σ1,Φ1⟩ −→ ⟨Σ2,Φ2⟩ (see Fig. 1). In [12] it is argued that such a situation occurs naturally when composing implementations of presentations or instanti- ating parametrized presentations. The Modularization Theorem for FOL speci- fications allows us to materialize the top right corner by construction.