Log in

Relevant bibliographies by topics / Craig's interpolation / Journal articles

Journal articles on the topic 'Craig's interpolation'

To see the other types of publications on this topic, follow the link: Craig's interpolation.

Author: Grafiati

Published: 14 March 2023

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the top 50 journal articles for your research on the topic 'Craig's interpolation.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Browse journal articles on a wide variety of disciplines and organise your bibliography correctly.

1

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

2

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

3

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

Full text

Abstract:

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].

APA, Harvard, Vancouver, ISO, and other styles

4

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

Full text

Abstract:

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?

APA, Harvard, Vancouver, ISO, and other styles

5

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

6

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

7

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

8

Molnár, Zalán, and Ö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.

Full text

APA, Harvard, Vancouver, ISO, and other styles

9

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

10

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

11

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

12

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

13

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

14

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

15

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

16

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

17

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

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

18

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

19

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

20

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

21

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

22

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

23

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

24

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

25

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

26

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

27

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

28

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

29

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

30

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

31

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

32

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

33

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

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.

Full text

APA, Harvard, Vancouver, ISO, and other styles

35

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

36

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

37

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

38

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

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 (July 1995): 364–81. http://dx.doi.org/10.1305/ndjfl/1040149353.

Full text

APA, Harvard, Vancouver, ISO, and other styles

40

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

41

Artale, Alessandro, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, and 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 (May 18, 2021): 6193–201. http://dx.doi.org/10.1609/aaai.v35i7.16770.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

42

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

43

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

44

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

45

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

46

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

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

47

Weaver, George, and 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 (December 1986): 969–80. http://dx.doi.org/10.2307/2273909.

Full text

Abstract:

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]).

APA, Harvard, Vancouver, ISO, and other styles

48

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

49

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

Full text

Abstract:

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].

APA, Harvard, Vancouver, ISO, and other styles

50

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

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!