1,721,273 research outputs found
All intermediate logics with extra axioms in one variable, except eight, are not strongly omega-complete
No full textIn [8] it is proved that all the intermediate logics axiomatizable by formulas in one variable, except four of them, are not strongly complete. We considerably improve this result by showing that all the intermediate logics axiomatizable by formulas in one variable, except eight of them, are not strongly -complete. Thus, a definitive classification of such logics with respect to the notions of canonicity, strong completeness, -canonicity and strong -completeness is given
Terminating sequent calculi for proving and refuting formulas in S4
No full textWe present a contraction-free sequent calculus GS4 for the modal logic S4 such that all the rules are decreasing and enjoy the subformula property. We also introduce a refutation calculus RS4 with the same properties of GS4. We provide a proof search algorithm that, given a sequent σ, returns either a proof of σ in GS4 or a refutation of σ in RS4. From a refutation of σ, we can generate an S4-model of σ
Hypercanonicity, extensive canonicity, canonicity and strong completeness of intermediate propositional logics
Full text linkThe paper investigates some questions concerning canonicity and strong completeness of intermediate propositional logics. We propose a refined classification of canonicity, distinguishing some kinds of ``subcanonicity'', we call hypercanonicity and extensive canonicity. Then, we state some criteria for the classification of logics according to these notions, and we give some applications to well known logics, such as the logics axiomatized by formulas in one variable and Medvedev logic
Kripke completeness for intermediate logics
Full text linkThe thesis studies problems in model theory for nonclassical logics, more specifically, for intermediate propositional logics. This area was opened in the 1930s by the well-known works of Gödel and Tarski and has now evolved into an interesting and complex mathematical field, with a strong trend to Computer Science applications. Kripke semantics has revealed a powerful instrument for studying their syntactic and computational properties and also for deeper understanding of constructivity. Fundamental results in Kripke semantics were proved in the last thirty years; many of them are collected in the recent book ``Modal logic'' by A. Chagrov and M. Zakharyaschev (1997). However several important problems in this field are still open, for example, little is known about completeness/incompleteness properties of intermediate logics; this is the main subject of the thesis. We consider several variants of completeness; in their increasing strength they are: hypercanonicity, extensive canonicity, canonicity, and strong completeness. We also introduce weaker versions of these properties, namely ω-hypercanonicity, extensive ω-canonicity, ω-strong completeness. This classification is shown to be nontrivial even within the well-known intermediate logics, such as logics axiomatized by one-variable formulas, logics of finite trees and some others. We develop new techniques, which have a general interest and can be applied when Kripke semantics is concerned.
More in detail:
- We prove some criteria to state canonicity, strong completeness, ω-canonicity, strong ω-completeness of intermediate logics.
- We give some results about classifications of intermediate logics with respect to these notions. In particular, we prove the significant result that all intermediate logics axiomatized by formulas in one variable (Nishimura formulas), except eight of them, are not strongly ω-complete
A cut-free sequent calculus for the logic of constant domains with a limited amount of duplications
Full text linkCut-free sequent calculi for the predicate intermediate logic CD of constant domains have appeared only
very recently in literature, even if this logic has been axiomatized since the early seventies. In the present
paper we propose a different cut-free sequent calculus for CD, in which a great care is devoted in avoiding
duplications of formulas
Model Validation through CooML Snapshot Generation
No full textThe object of this paper is model validation, namely the study of the “correctness” of formal specifications (or models) with respect to their requirements. Since requirements are informal, validation can be only experimental. In the UML, snapshot generation has been proposed as a tool for validating class diagrams and contracts. Snapshots are object diagrams representing the possible system states, where one compares the snapshots generated from the UML model with the expected ones. In this paper we present a DLV implementation of snapshot generation for CooML (Constructive
Object Oriented Modeling Language), a modeling language based on a constructive semantics we are developing.We firstly explain CooML snapshot semantics and we show by an example how UML class diagrams with OCL constraints can be represented in CooML. Then we explain our implementation of CooML snapshot generation in DLV and discuss its potential application for model validation
Connections Between Answer Set Semantics and Information Terms Semantics in Constructive EL_bot (Extended Abstract)
Full text linkA Natural Deduction Calculus for Godel-Dummett Logic Internalizing Proof-search Control Mechanisms
Full text linkWe introduce a natural deduction calculus for the G ̈odelDummett Logic LC semantically characterized by linearly ordered Kripke models. Our calculus is inspired by an analogous calculus for Intuitionistic logic (IPL) internalizing mechanisms to reduce the proof-search space that has been used to define a goal-oriented proof-search procedure for IPL. In this paper we present the calculus for LC and we sketch its soundness and completeness
- …
