1,721,041 research outputs found
Valutare l'istituzione delle aree contigue per fini ambientali nel Parco del Trasimeno: un esperimento di scelta
No full textProof theory for locally finite many-valued logics: semi-projective logics
No full textWe extend a methodology by Baaz and Fermüller to systematically construct analytic calculi for semi-projective logics—a large family of (propositional) locally finite many-valued logics. Our calculi, defined in the framework of sequents of relations, are proof search oriented and can be used to settle the computational complexity of the formalized logics. As a case study we derive sequent calculi of relations for Nilpotent Minimum logic and for Hajek’s Basic Logic extended with the n-contraction axiom (n ≥ 1)
Uniform proofs of standard completeness for extensions of first-order MTL
Full text linkWe provide general - and automatedly verifiable - sufficient conditions that ensure standard completeness for logics formalized Hilbert-style. Our approach subsumes many existing results and allows for the discovery of new fuzzy logics which extend first-order Monoidal T-norm Logic with propositional axioms
Analytic Calculi for Monoidal T-norm Based Logic
No full textMonoidal t-norm based logic MTL is the logic of left continuous t-norms. We introduce two analytic calculi for first-order MTL. These are obtained by lifting two sequent calculi for different fragments of this logic to the hypersequent level with subsequent addition of Avron's communication rule. Our calculi enable to prove the mid(hyper)sequent theorem. As corollaries follow Herbrand's theorem for first-order MTL, the decidability of its For AllThere Exists-fragment and admissibility of Skolemization
Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions
No full textExtensions of monoidal t-norm logic MTL and related fuzzy logics with truth stresser modalities such as globalization and "very true" are presented here both algebraically in the framework of residuated lattices and proof-theoretically as hypersequent calculi. Completeness with respect to standard algebras based on t-norms, embeddings between logics, decidability, and the finite embedding property are then investigated for these logics
Hypertableau and path-hypertableau calculi for some families of intermediate logics
No full textIn this paper we investigate the tableau systems corresponding to hypersequent calculi. We call these systems hypertableau calculi. We define hypertableau calculi for some propositional intermediate logics. We then introduce path-hypertableau calculi which are simply defined by imposing additional structure on hypertableaux. Using path-hypertableaux we define analytic calculi for the intermediate logics \Bd_k, with , which are semantically characterized by Kripke models of depth . These calculi are obtained by adding one more structural rule to the path-hypertableau calculus for Intuitionistic Logic
- …
