Bibliographies thématiques / Craig's interpolation / Articles de revues

Articles de revues sur le sujet « Craig's interpolation »

Pour voir les autres types de publications sur ce sujet consultez le lien suivant : Craig's interpolation.
Auteur : Grafiati
Publié le 14 mars 2023

Créez une référence correcte selon les styles APA, MLA, Chicago, Harvard et plusieurs autres

Choisissez une source :

Consultez les 50 meilleurs articles de revues pour votre recherche sur le sujet « Craig's interpolation ».

À côté de chaque source dans la liste de références il y a un bouton « Ajouter à la bibliographie ». Cliquez sur ce bouton, et nous générerons automatiquement la référence bibliographique pour la source choisie selon votre style de citation préféré : APA, MLA, Harvard, Vancouver, Chicago, etc.

Vous pouvez aussi télécharger le texte intégral de la publication scolaire au format pdf et consulter son résumé en ligne lorsque ces informations sont inclues dans les métadonnées.

Parcourez les articles de revues sur diverses disciplines et organisez correctement votre bibliographie.

1

Beklemishev, L. D. « Provability logic without Craig's interpolation property ». Mathematical Notes of the Academy of Sciences of the USSR 45, no 6 (juin 1989) : 437–45. http://dx.doi.org/10.1007/bf01158230.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
2

Maffezioli, Paolo, et Eugenio Orlandelli. « Full Cut Elimination and Interpolation for Intuitionistic Logic with Existence Predicate ». Bulletin of the Section of Logic 48, no 2 (30 juin 2019) : 137–58. http://dx.doi.org/10.18778/0138-0680.48.2.04.

Texte intégral
Résumé :
In previous work by Baaz and Iemhoff, a Gentzen calculus for intuitionistic logic with existence predicate is presented that satisfies partial cut elimination and Craig's interpolation property; it is also conjectured that interpolation fails for the implication-free fragment. In this paper an equivalent calculus is introduced that satisfies full cut elimination and allows a direct proof of interpolation via Maehara's lemma. In this way, it is possible to obtain much simpler interpolants and to better understand and (partly) overcome the failure of interpolation for the implication-free fragment.
Styles APA, Harvard, Vancouver, ISO, etc.
3

Sági, Gábor, et Saharon Shelah. « On weak and strong interpolation in algebraic logics ». Journal of Symbolic Logic 71, no 1 (mars 2006) : 104–18. http://dx.doi.org/10.2178/jsl/1140641164.

Texte intégral
Résumé :
AbstractWe show that there is a restriction, or modification of the finite-variable fragments of First Order Logic in which a weak form of Craig's Interpolation Theorem holds but a strong form of this theorem does not hold. Translating these results into Algebraic Logic we obtain a finitely axiomatizable subvariety of finite dimensional Representable Cylindric Algebras that has the Strong Amalgamation Property but does not have the Superamalgamation Property. This settles a conjecture of Pigozzi [12].
Styles APA, Harvard, Vancouver, ISO, etc.
4

Mason, Ian. « The metatheory of the classical propositional calculus is not axiomatizable ». Journal of Symbolic Logic 50, no 2 (juin 1985) : 451–57. http://dx.doi.org/10.2307/2274233.

Texte intégral
Résumé :
In this paper we investigate the first order metatheory of the classical propositional logic. In the first section we prove that the first order metatheory of the classical propositional logic is undecidable. Thus as a mathematical object even the simplest of logics is, from a logical standpoint, quite complex. In fact it is of the same complexity as true first order number theory.This result answers negatively a question of J. F. A. K. van Benthem (see [van Benthem and Doets 1983]) as to whether the interpolation theorem in some sense completes the metatheory of the calculus. Let us begin by motivating the question that we answer. In [van Benthem and Doets 1983] it is claimed that a folklore prejudice has it that interpolation was the final elementary property of first order logic to be discovered. Even though other properties of the propositional calculus have been discovered since Craig's orginal paper [Craig 1957] (see for example [Reznikoff 1965]) there is a lot of evidence for the fundamental nature of the property. In abstract model theory for example one finds that very few logics have the interpolation property. There are two well-known open problems in this area. These are1. Is there a logic satisfying the full compactness theorem as well as the interpolation theorem that is not equivalent to first order logic even for finite models?2. Is there a logic stronger than L(Q), the logic with the quantifierthere exist uncountably many, that is countably compact and has the interpolation property?
Styles APA, Harvard, Vancouver, ISO, etc.
5

Ono, Hiroakira. « Craig's interpolation theorem for the intuitionistic logic and its extensions—A semantical approach ». Studia Logica 45, no 1 (mars 1986) : 19–33. http://dx.doi.org/10.1007/bf01881546.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
6

ALIZADEH, MAJID, FARZANEH DERAKHSHAN et HIROAKIRA ONO. « UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS ». Review of Symbolic Logic 7, no 3 (27 mai 2014) : 455–83. http://dx.doi.org/10.1017/s175502031400015x.

Texte intégral
Résumé :
AbstractUniform interpolation property of a given logic is a stronger form of Craig’s interpolation property where both pre-interpolant and post-interpolant always exist uniformly for any provable implication in the logic. It is known that there exist logics, e.g., modal propositional logic S4, which have Craig’s interpolation property but do not have uniform interpolation property. The situation is even worse for predicate logics, as classical predicate logic does not have uniform interpolation property as pointed out by L. Henkin.In this paper, uniform interpolation property of basic substructural logics is studied by applying the proof-theoretic method introduced by A. Pitts (Pitts, 1992). It is shown that uniform interpolation property holds even for their predicate extensions, as long as they can be formalized by sequent calculi without contraction rules. For instance, uniform interpolation property of full Lambek predicate calculus, i.e., the substructural logic without any structural rule, and of both linear and affine predicate logics without exponentials are proved.
Styles APA, Harvard, Vancouver, ISO, etc.
7

Rodenburg, P. H. « Interpolation in Conditional Equational Logic1 ». Fundamenta Informaticae 15, no 1 (1 juin 1991) : 80–85. http://dx.doi.org/10.3233/fi-1991-15106.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
8

Molnár, Zalán, et Öztürk Övge. « Notes on localizing Craig’s interpolation theorem ». Elpis. Filozófiatudományi Folyóirat 15, no 1-2 (2022) : 103–16. http://dx.doi.org/10.54310/elpis.2022.1.8.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
9

Kowalski, Tomasz. « PDL has interpolation ». Journal of Symbolic Logic 67, no 3 (septembre 2002) : 933–46. http://dx.doi.org/10.2178/jsl/1190150141.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
10

Feferman, Solomon. « Harmonious logic : Craig’s interpolation theorem and its descendants ». Synthese 164, no 3 (1 juillet 2008) : 341–57. http://dx.doi.org/10.1007/s11229-008-9354-2.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
11

Kuznets, Roman, et Björn Lellmann. « Interpolation for intermediate logics via injective nested sequents ». Journal of Logic and Computation 31, no 3 (avril 2021) : 797–831. http://dx.doi.org/10.1093/logcom/exab015.

Texte intégral
Résumé :
Abstract We introduce a novel, semantically inspired method of constructing nested sequent calculi for propositional intermediate logics. Applying recently developed methods for proving Craig interpolation to these nested sequent calculi, we obtain constructive proofs of the interpolation property for most non-trivial interpolable intermediate logics, as well as Lyndon interpolation for Gödel logic. Finally, we provide a prototype implementation combining proof search and countermodel construction.
Styles APA, Harvard, Vancouver, ISO, etc.
12

Marchioni, Enrico, et George Metcalfe. « Craig interpolation for semilinear substructural logics ». Mathematical Logic Quarterly 58, no 6 (19 octobre 2012) : 468–81. http://dx.doi.org/10.1002/malq.201200004.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
13

Jerome Keisler, H., et Jeffrey M. Keisler. « Craig interpolation for networks of sentences ». Annals of Pure and Applied Logic 163, no 9 (septembre 2012) : 1322–44. http://dx.doi.org/10.1016/j.apal.2012.03.001.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
14

Maksimova, L. L. « The decidability of craig’s interpolation property in well-composed J-logics ». Siberian Mathematical Journal 53, no 5 (septembre 2012) : 839–52. http://dx.doi.org/10.1134/s0037446612050096.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
15

Wernhard, Christoph. « Craig Interpolation with Clausal First-Order Tableaux ». Journal of Automated Reasoning 65, no 5 (27 mai 2021) : 647–90. http://dx.doi.org/10.1007/s10817-021-09590-3.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
16

Leroux, Jérôme, Philipp Rümmer et Pavle Subotić. « Guiding Craig interpolation with domain-specific abstractions ». Acta Informatica 53, no 4 (15 mai 2015) : 387–424. http://dx.doi.org/10.1007/s00236-015-0236-z.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
17

Salibra, Antonino, et Giuseppe Scollo. « Interpolation and compactness in categories of pre-institutions ». Mathematical Structures in Computer Science 6, no 3 (juin 1996) : 261–86. http://dx.doi.org/10.1017/s0960129500001006.

Texte intégral
Résumé :
An analysis of relationships between Craig-style interpolation, compactness, and other related model-theoretic properties is carried out in the softer framework of categories of pre-institutions. While the equivalence between sentence interpolation and the Robinson property under compactness and Boolean closure is well known, a similar result under different assumptions (not involving compactness) is newly established for presentation interpolation. The standard concept of naturality of model transformation is enriched by a new property, termed restriction adequacy, which proves useful for the reduction of interpolation along pre-institution transformations. A distinct reduction theorem for the Robinson property is presented as well. A variant of the ultraproduct concept is further introduced, and the related closure property for pre-institutions is shown to be equivalent to compactness
Styles APA, Harvard, Vancouver, ISO, etc.
18

OLKHOVIKOV, GRIGORY K. « RESTRICTED INTERPOLATION AND LACK THEREOF IN STIT LOGIC ». Review of Symbolic Logic 13, no 3 (13 septembre 2019) : 459–82. http://dx.doi.org/10.1017/s1755020319000406.

Texte intégral
Résumé :
AbstractWe consider the propositional logic equipped with Chellas stit operators for a finite set of individual agents plus the historical necessity modality. We settle the question of whether such a logic enjoys restricted interpolation property, which requires the existence of an interpolant only in cases where the consequence contains no Chellas stit operators occurring in the premise. We show that if action operators count as logical symbols, then such a logic has restricted interpolation property iff the number of agents does not exceed three. On the other hand, if action operators are considered to be nonlogical symbols, then the restricted interpolation fails for any number of agents exceeding one. It follows that unrestricted Craig interpolation also fails for almost all versions of stit logic.
Styles APA, Harvard, Vancouver, ISO, etc.
19

Diaconescu, Răzvan. « An Institution-independent Proof of Craig Interpolation Theorem ». Studia Logica 77, no 1 (juin 2004) : 59–79. http://dx.doi.org/10.1023/b:stud.0000034185.62660.d6.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
20

Rümmer, Philipp, Hossein Hojjat et Viktor Kuncak. « On recursion-free Horn clauses and Craig interpolation ». Formal Methods in System Design 47, no 1 (3 décembre 2014) : 1–25. http://dx.doi.org/10.1007/s10703-014-0219-7.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
21

Rasga, João, Cristina Sernadas et Amlcar Sernadas. « Craig Interpolation in the Presence of Unreliable Connectives ». Logica Universalis 8, no 3-4 (2 avril 2014) : 423–46. http://dx.doi.org/10.1007/s11787-014-0101-9.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
22

Väänänen, Jouko. « The Craig Interpolation Theorem in abstract model theory ». Synthese 164, no 3 (1 juillet 2008) : 401–20. http://dx.doi.org/10.1007/s11229-008-9357-z.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
23

KOWALSKI, TOMASZ, et HIROAKIRA ONO. « ANALYTIC CUT AND INTERPOLATION FOR BI-INTUITIONISTIC LOGIC ». Review of Symbolic Logic 10, no 2 (6 décembre 2016) : 259–83. http://dx.doi.org/10.1017/s175502031600040x.

Texte intégral
Résumé :
AbstractWe prove that certain natural sequent systems for bi-intuitionistic logic have the analytic cut property. In the process we show that the (global) subformula property implies the (local) analytic cut property, thereby demonstrating their equivalence. Applying a version of Maehara technique modified in several ways, we prove that bi-intuitionistic logic enjoys the classical Craig interpolation property and Maximova variable separation property; its Halldén completeness follows.
Styles APA, Harvard, Vancouver, ISO, etc.
24

Ren, Xuanzhi. « Fullness and Decidability in Continuous Propositional Logic ». Mathematics 10, no 23 (25 novembre 2022) : 4455. http://dx.doi.org/10.3390/math10234455.

Texte intégral
Résumé :
In this paper we consider general continuous propositional logics and prove some basic properties about them. First, we characterize full systems of continuous connectives of the form {¬,,f} where f is a unary connective. We also show that, in contrast to the classical propositional logic, a full system of continuous propositional logic cannot contain only one continuous connective. We then construct a closed full system of continuous connectives without any constants. Such a system does not have any tautologies. For the rest of the paper we consider the standard continuous propositional logic as defined by Yaacov, I.B and Usvyatsov, A. We show that Strong Compactness and Craig Interpolation fail for this logic, but approximated versions of Strong Compactness and Craig Interpolation hold true. In the last part of the paper, we introduce various notions of satisfiability, falsifiability, tautology, and fallacy, and show that they are either NP-complete or co-NP-complete.
Styles APA, Harvard, Vancouver, ISO, etc.
25

Liu, Ying, Hongguang Li, Yun Li et Huanyu Du. « A Component-Based Parametric Reduced-Order Modeling Method Combined with Substructural Matrix Interpolation and Automatic Sampling ». Shock and Vibration 2019 (8 juillet 2019) : 1–14. http://dx.doi.org/10.1155/2019/6407437.

Texte intégral
Résumé :
An efficient parametric reduced-order modeling method combined with substructural matrix interpolation and automatic sampling procedure is proposed. This approach is based on the fixed-interface Craig-Bampton component mode synthesis method (CMS). The novel parametric reduced-order models (PROMs) are developed by interpolating substructural reduced-order matrices. To guarantee the compatibility of the coordinates, we develop a three-step adjustment procedure by reducing the local interface degrees of freedom (DOFs) and performing congruence transformation for the normal modes and interface reduced basis, respectively. In addition, an automatic sampling process is also introduced to dynamically fulfill the predefined error limits. It proceeds by first exploring the parameter space and identifying the sampling points with maximum error indicators for all the parameter-dependent substructures. The exact error of the assembled model at the optimal parameter point is subsequently calculated to determine whether the automatic sampling procedure reaches a desired error tolerance. The proposed framework is then applied to the moving coil of electrical-dynamic shaker to illustrate the advantage and validity. The results indicate that this new approach can significantly reduce both the offline database construction time and online calculation time. Besides, the automatic procedure can sample the parameter space efficiently and fulfill the stopping criterion dynamically with assurance of the resulting PROM accuracy.
Styles APA, Harvard, Vancouver, ISO, etc.
26

Esparza, Javier, Stefan Kiefer et Stefan Schwoon. « Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems1 ». Journal on Satisfiability, Boolean Modeling and Computation 5, no 1-4 (1 juin 2008) : 27–56. http://dx.doi.org/10.3233/sat190051.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
27

Kamide, Norihiro. « Notes on Craig interpolation for LJ with strong negation ». Mathematical Logic Quarterly 57, no 4 (11 mars 2011) : 395–99. http://dx.doi.org/10.1002/malq.201010016.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
28

Seldin, Jonathan P. « On the proof theory of the intermediate logic MH ». Journal of Symbolic Logic 51, no 3 (septembre 1986) : 626–47. http://dx.doi.org/10.2307/2274019.

Texte intégral
Résumé :
AbstractA natural deduction formulation is given for the intermediate logic called MH by Gabbay in [4]. Proof-theoretic methods are used to show that every deduction can be normalized, that MH is the weakest intermediate logic for which the Glivenko theorem holds, and that the Craig-Lyndon interpolation theorem holds for it.
Styles APA, Harvard, Vancouver, ISO, etc.
29

Mancosu, Paolo. « Introduction : Interpolations—Essays in honor of William Craig ». Synthese 164, no 3 (24 juin 2008) : 313–19. http://dx.doi.org/10.1007/s11229-008-9350-6.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
30

Chen, Zhi Yuan, Shao Bin Huang et Li Li Han. « A Fast Approach of Locating Complex System Design Errors ». Key Engineering Materials 572 (septembre 2013) : 115–18. http://dx.doi.org/10.4028/www.scientific.net/kem.572.115.

Texte intégral
Résumé :
Model checking technique can give a specific counterexample which explains how the system violates some assertion when model does not satisfy the specification. However, it is a tedious work to understand the long counterexamples. We propose a genetic algorithm to enhance the efficiency of understanding long counterexample by computing the minimal unsatisfiable subformula. Besides, we also propose a Craig interpolation computation-based method to understand counterexample. The causes which are responsible for model failure are extracted by deriving interpolation from the proof of the nonsatisfiability of the initial state and the weakest precondition of counterexample. Experimental results show that our methods improve the efficiency of understanding counterexamples and debugging significantly.
Styles APA, Harvard, Vancouver, ISO, etc.
31

Ahmed, Tarek. « Representability and amalgamation for Heyting polyadic algebras ». Studia Scientiarum Mathematicarum Hungarica 48, no 4 (1 décembre 2011) : 509–39. http://dx.doi.org/10.1556/sscmath.48.2011.4.1190.

Texte intégral
Résumé :
We prove that every (not necessarily locally finite) polyadic Heyting algebra of infinite dimension is representable in some concrete sense. We also show that this class has the super amalgamation property. As a byproduct we infer that a certain infinitary extension of predicate intuitionistic logic, or equivalently, the intuitionistic fragment of Keisler’s infinitary logics, is complete and enjoys the Craig interpolation property.
Styles APA, Harvard, Vancouver, ISO, etc.
32

Krajíček, Jan. « Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic ». Journal of Symbolic Logic 62, no 2 (juin 1997) : 457–86. http://dx.doi.org/10.2307/2275541.

Texte intégral
Résumé :
AbstractA proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1)Feasible interpolation theorems for the following proof systems:(a)resolution(b)a subsystem of LK corresponding to the bounded arithmetic theory (α)(c)linear equational calculus(d)cutting planes.(2)New proofs of the exponential lower bounds (for new formulas)(a)for resolution ([15])(b)for the cutting planes proof system with coefficients written in unary ([4]).(3)An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory (α).In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle.
Styles APA, Harvard, Vancouver, ISO, etc.
33

Sernadas, C., J. Rasga et A. Sernadas. « Preservation of Craig interpolation by the product of matrix logics ». Journal of Applied Logic 11, no 3 (septembre 2013) : 328–49. http://dx.doi.org/10.1016/j.jal.2013.06.001.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
34

Goranko, Valentin. « The Craig interpolation theorem for prepositional logics with strong negation ». Studia Logica 44, no 3 (1985) : 291–317. http://dx.doi.org/10.1007/bf00394448.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
35

Карпенко, А. С. « Von Wright’s truth-logic and around ». Logical Investigations 19 (9 avril 2013) : 39–50. http://dx.doi.org/10.21146/2074-1472-2013-19-0-39-50.

Texte intégral
Résumé :
In this paper von Wright’s truth-logic T__ is considered. It seems that it is a De Morgan four-valued logic DM4 (or Belnap’s four-valued logic) with endomorphism e2. In connection with this many other issues are discussed: twin truth operators, a truth-logic with endomorphism g (or logic Tr), the lattice of extensions of DM4, modal logic V2, Craig interpolation property, von Wright–Segerberg’s tense logic W, and so on.
Styles APA, Harvard, Vancouver, ISO, etc.
36

Akhin, Marat, Sam Kolton et Vladimir Itsykson. « Random model sampling : Making craig interpolation work when it should not ». Automatic Control and Computer Sciences 49, no 7 (décembre 2015) : 413–19. http://dx.doi.org/10.3103/s0146411615070020.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
37

Akhin, Marat, Sam Kolton et Vladimir Itsykson. « Random Model Sampling : Making Craig Interpolation Work When It Should Not ». Modeling and Analysis of Information Systems 21, no 6 (1 janvier 2014) : 7–17. http://dx.doi.org/10.18255/1818-1015-2014-6-7-17.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
38

Hanazawa, Masazumi, et Mitio Takano. « An interpolation theorem in many-valued logic ». Journal of Symbolic Logic 51, no 2 (juin 1986) : 448–52. http://dx.doi.org/10.1017/s0022481200031315.

Texte intégral
Résumé :
A many-valued logic version of the Craig-Lyndon interpolation theorem has been given by Gill [1] and Miyama [2]. The former dealt with three-valued logic and the latter generalized it to M-valued logic with M ≥ 3. The purpose of this paper is to improve the form of Miyama's version of the interpolation theorem. The system used in this paper is a many-valued analogue (Takahashi [4], Rousseau [3]) of Gentzen's logical calculus LK. Let T = {1,…, M} be the set of truth values. An M-tuple (Γ1,…, ΓM) of sets of formulas is called a sequent, which is regarded as valid if for any valuation (in canonical sense) there is a truth value μ Є T such that the set Γμ contains a formula of the value μ with respect to the valuation. (In the next section, and thereafter, we change the format of the sequent for typographical reasons.) Miyama's result is as follows (in representative form):(I) If a sequent ({A}, ∅,…, ∅, {B}) is valid, then there is a formula D such that(i) every predicate or propositional variable occurring in D occurs in A and B, and(ii) the sequents {{A}, ∅,…, ∅, {D}) and (D}, ∅,…, ∅, {B}) are both valid.What shall be proved in this paper is the following (in representative form):(II) If a sequent ({A1}, {A2}, …, {AM}) is valid, then there is a formula D such that(i) every predicate or propositional variable occurring in D occurs in at least two of the formulas A1,…, AM, and(ii) the following M sequents are valid:({A1},{D},…,{D}),({D},{A2},…,{D}),…,({D},{D},…,{AM}).Clearly the former can be obtained as a corollary of the latter.
Styles APA, Harvard, Vancouver, ISO, etc.
39

Makkai, Michael. « On Gabbay's Proof of the Craig Interpolation Theorem for Intuitionistic Predicate Logic ». Notre Dame Journal of Formal Logic 36, no 3 (juillet 1995) : 364–81. http://dx.doi.org/10.1305/ndjfl/1040149353.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
40

Jain, Himanshu, Edmund M. Clarke et Orna Grumberg. « Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations ». Formal Methods in System Design 35, no 1 (24 avril 2009) : 6–39. http://dx.doi.org/10.1007/s10703-009-0069-x.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
41

Artale, Alessandro, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki et Frank Wolter. « Living Without Beth and Craig : Definitions and Interpolants in Description Logics with Nominals and Role Inclusions ». Proceedings of the AAAI Conference on Artificial Intelligence 35, no 7 (18 mai 2021) : 6193–201. http://dx.doi.org/10.1609/aaai.v35i7.16770.

Texte intégral
Résumé :
The Craig interpolation property (CIP) states that an interpolant for an implication exists iff it is valid. The projective Beth definability property (PBDP) states that an explicit definition exists iff a formula stating implicit definability is valid. Thus, the CIP and PBDP transform potentially hard existence problems into deduction problems in the underlying logic. Description Logics with nominals and/or role inclusions do not enjoy the CIP nor PBDP, but interpolants and explicit definitions have many potential applications in ontology engineering and ontology-based data management. In this article we show the following: even without Craig and Beth, the existence of interpolants and explicit definitions is decidable in description logics with nominals and/or role inclusions such as ALCO, ALCH and ALCHIO. However, living without Craig and Beth makes this problem harder than deduction: we prove that the existence problems become 2EXPTIME-complete, thus one exponential harder than validity. The existence of explicit definitions is 2EXPTIME-hard even if one asks for a definition of a nominal using any symbol distinct from that nominal, but it becomes EXPTIME-complete if one asks for a definition of a concept name using any symbol distinct from that concept name.
Styles APA, Harvard, Vancouver, ISO, etc.
42

Ignatiev, Konstantin N. « On strong provability predicates and the associated modal logics ». Journal of Symbolic Logic 58, no 1 (mars 1993) : 249–90. http://dx.doi.org/10.2307/2275337.

Texte intégral
Résumé :
AbstractPA is Peano Arithmetic. Pr(x) is the usual Σ1,-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ1. An example: Q is ω-provable if PA + ¬Q is ω-inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω-provability and obtained its arithmetical completeness.In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point property and the Craig interpolation lemma. We also consider other examples of the strong provability predicates and their applications.
Styles APA, Harvard, Vancouver, ISO, etc.
43

Montagna, Franco. « Δ-core Fuzzy Logics with Propositional Quantifiers, Quantifier Elimination and Uniform Craig Interpolation ». Studia Logica 100, no 1-2 (9 février 2012) : 289–317. http://dx.doi.org/10.1007/s11225-012-9379-x.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
44

BÁRÁNY, VINCE, MICHAEL BENEDIKT et BALDER TEN CATE. « SOME MODEL THEORY OF GUARDED NEGATION ». Journal of Symbolic Logic 83, no 04 (décembre 2018) : 1307–44. http://dx.doi.org/10.1017/jsl.2018.64.

Texte intégral
Résumé :
AbstractThe Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this article we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics.
Styles APA, Harvard, Vancouver, ISO, etc.
45

Toman, David, et Grant Weddell. « First Order Rewritability in Ontology-Mediated Querying in Horn Description Logics ». Proceedings of the AAAI Conference on Artificial Intelligence 36, no 5 (28 juin 2022) : 5897–905. http://dx.doi.org/10.1609/aaai.v36i5.20534.

Texte intégral
Résumé :
We consider first-order (FO) rewritability for query answering in ontology mediated querying (OMQ) in which ontologies are formulated in Horn fragments of description logics (DLs). In general, OMQ approaches for such logics rely on non-FO rewriting of the query and/or on non-FO completion of the data, called a ABox. Specifically, we consider the problem of FO rewritability in terms of Beth definability, and show how Craig interpolation can then be used to effectively construct the rewritings, when they exist, from the Clark’s completion of Datalog-like programs encoding a given DL TBox and optionally a query. We show how this approach to FO rewritability can also be used to (a) capture integrity constraints commonly available in backend relational data sources, (b) capture constraints inherent in mapping such sources to an ABox , and (c) can be used an alternative to deriving so-called perfect rewritings of queries in the case of DL-Lite ontologies.
Styles APA, Harvard, Vancouver, ISO, etc.
46

Bezhanishvili, Nick, et Tim Henke. « A model-theoretic approach to descriptive general frames : the van Benthem characterization theorem ». Journal of Logic and Computation 30, no 7 (26 août 2020) : 1331–55. http://dx.doi.org/10.1093/logcom/exaa040.

Texte intégral
Résumé :
Abstract The celebrated van Benthem characterization theorem states that on Kripke structures modal logic is the bisimulation-invariant fragment of first-order logic. In this paper, we prove an analogue of the van Benthem characterization theorem for models based on descriptive general frames. This is an important class of general frames for which every modal logic is complete. These frames can be represented as Stone spaces equipped with a ‘continuous’ binary relation. The proof of our theorem generalizes Rosen’s proof of the van Benthem theorem for finite frames and uses as an essential technique a new notion of descriptive unravelling. We also develop a basic model theory for descriptive general frames and show that in many ways it behaves like the model theory of finite structures. In particular, we prove the failure of the compactness theorem, of the Beth definability theorem, of the Craig interpolation theorem and of the upward Löwenheim–Skolem theorem.1
Styles APA, Harvard, Vancouver, ISO, etc.
47

Weaver, George, et Jeffrey Welaish. « Back and forth constructions in modal logic : An interpolation theorem for a family of modal logics ». Journal of Symbolic Logic 51, no 4 (décembre 1986) : 969–80. http://dx.doi.org/10.2307/2273909.

Texte intégral
Résumé :
The following is a contribution to the abstract study of the model theory of modal logics. Historically, individual modal logics have been specified deductively; and, as a result, it has seemed natural to view modal logics as sets of sentences provable in some deductive system. This proof theoretic view has influenced the abstract study of modal logics. For example, Fine [1975] defines a modal logic to be any set of sentences in the modal language L□ which contains all tautologies, all instances of the schema (□(ϕ ⊃ Ψ) ⊃ (□ϕ ⊃ □Ψ)), and which is closed under modus ponens, necessitation and substitution.Here, however, modal logics are equated with classes of “possible world” interpretations. “Worlds” are taken to be ordered pairs (a, λ), where a is a sentential interpretation and λ is an ordinal. Properties of the accessibility relation are identified with those classes of binary relational systems closed under isomorphisms. The origin of this approach is the study of alternative Kripke semantics for the normal modal logics (cf. Weaver [1973]). It is motivated by the desire that modal logics provide accounts of both logical truth and logical consequence (cf. Corcoran and Weaver [1969]) and the realization that there are alternative Kripke semantics for S4, B and M which give identical accounts of logical truth, but different accounts of logical consequence (cf. Weaver [1973]). It is shown that the Craig interpolation theorem holds for any modal logic which has characteristic modal axioms and whose associated class of binary relational systems is closed under subsystems and finite direct products. The argument uses a back and forth construction to establish a modal analogue of Robinson's theorem. The argument for the interpolation theorem from Robinson's theorem employs modal analogues of the Ehrenfeucht-Fraïssé characterization of elementary equivalence and Hintikka's distributive normal form, and is itself a modal analogue of a first order argument (cf. Weaver [1982]).
Styles APA, Harvard, Vancouver, ISO, etc.
48

Tan, Yung-Chang, Matthew P. Castanier et Christophe Pierre. « Approximation of Power Flow Between Two Coupled Beams Using Statistical Energy Methods ». Journal of Vibration and Acoustics 123, no 4 (1 avril 2001) : 510–23. http://dx.doi.org/10.1115/1.1399051.

Texte intégral
Résumé :
In this work, an investigation is performed into developing a general framework for predicting the power flow between coupled component structures with uncertain system parameters. A specific example of two coupled beams is considered, in which a torsional spring is attached at the coupling point to adjust the coupling strength. The power flow in the nominal system is formulated using component mode synthesis (CMS). First, the parameter-based statistical energy method, which employs free-interface component modes, is applied to obtain approximations for the ensemble-averaged power flow with each beam length having a uniformly-distributed random perturbation. Then, using fixed-interface component modes and constraint modes, the Craig-Bampton method of CMS is employed to formulate the nominal power flow equation in terms of the constraint-mode degrees of freedom. This fixed-interface CMS method is seen to provide a systematic and efficient platform for power flow analysis. Using this CMS basis, a general approximation for the ensemble-averaged power flow is formulated regardless of the probability distribution of the random parameters or the coupling strengths between the substructures. This approximation is derived using Galerkin’s method, in which each modal response is expanded in locally linear interpolation functions in the random system parameters. The proposed general framework is numerically validated by comparisons with wave approximations from the literature for this two-coupled-beam system.
Styles APA, Harvard, Vancouver, ISO, etc.
49

Mycielski, Jan. « Locally finite theories ». Journal of Symbolic Logic 51, no 1 (mars 1986) : 59–62. http://dx.doi.org/10.2307/2273942.

Texte intégral
Résumé :
We say that a first order theoryTislocally finiteif every finite part ofThas a finite model. It is the purpose of this paper to construct in a uniform way for any consistent theoryTa locally finite theory FIN(T) which is syntactically (in a sense) isomorphic toT.Our construction draws upon the main idea of Paris and Harrington [6] (I have been influenced by some unpublished notes of Silver [7] on this subject) and generalizes the syntactic aspect of their result from arithmetic to arbitrary theories. (Our proof is syntactic, and it is simpler than the proofs of [5], [6] and [7]. This reminds me of the simple syntactic proofs of several variants of the Craig-Lyndon interpolation theorem, which seem more natural than the semantic proofs.)The first mathematically strong locally finite theory, called FIN, was defined in [1] (see also [2]). Now we get much stronger ones, e.g. FIN(ZF).From a physicalistic point of view the theorems of ZF and their FIN(ZF)-counterparts may have the same meaning. Therefore FIN(ZF) is a solution of Hilbert's second problem. It eliminates ideal (infinite) objects from the proofs of properties of concrete (finite) objects.In [4] we will demonstrate that one can develop a direct finitistic intuition that FIN(ZF) is locally finite. We will also prove a variant of Gödel's second incompleteness theorem for the theory FIN and for all its primitively recursively axiomatizable consistent extensions.The results of this paper were announced in [3].
Styles APA, Harvard, Vancouver, ISO, etc.
50

Coscarelli, Bruno Costa. « Model Theory in a Paraconsistent Environment ». Bulletin of Symbolic Logic 27, no 2 (juin 2021) : 216. http://dx.doi.org/10.1017/bsl.2021.33.

Texte intégral
Résumé :
AbstractThe purpose of this thesis is to develop a paraconsistent Model Theory. The basis for such a theory was launched by Walter Carnielli, Marcelo Esteban Coniglio, Rodrigo Podiack, and Tarcísio Rodrigues in the article ‘On the Way to a Wider Model Theory: Completeness Theorems for First-Order Logics of Formal Inconsistency’ [The Review of Symbolic Logic, vol. 7 (2014)].Naturally, a complete theory cannot be fully developed in a single work. Indeed, the goal of this work is to show that a paraconsistent Model Theory is a sound and worthy possibility. The pursuit of this goal is divided in three tasks: The first one is to give the theory a philosophical meaning. The second one is to transpose as many results from the classical theory to the new one as possible. The third one is to show an application of the theory to practical science.The response to the first task is a Paraconsistent Reasoning System. The start point is that paraconsistency is an epistemological concept. The pursuit of a deeper understanding of the phenomenon of paraconsistency from this point of view leads to a reasoning system based on the Logics of Formal Inconsistency. Models are regarded as states of knowledge and the concept of isomorphism is reformulated so as to give raise to a new concept that preserves a portion of the whole knowledge of each state. Based on this, a notion of refinement is created which may occur from inside or from outside the state.In order to respond to the second task, two important classical results, namely the Omitting Types Theorem and Craig’s Interpolation Theorem are shown to hold in the new system and it is also shown that, if classical results in general are to hold in a paraconsistent system, then such a system should be in essence how it was developed here.Finally, the response to the third task is a proposal of what a Paraconsistent Logic Programming may be. For that, the basis for a paraconsistent PROLOG is settled in the light of the ideas developed so far.Abstract prepared by Bruno Costa Coscarelli.E-mail: brunocostacoscarelli@gmail.comURL: http://repositorio.unicamp.br/jspui/handle/REPOSIP/331697
Styles APA, Harvard, Vancouver, ISO, etc.
Nous offrons des réductions sur tous les plans premium pour les auteurs dont les œuvres sont incluses dans des sélections littéraires thématiques. Contactez-nous pour obtenir un code promo unique!

Vers la bibliographie