scholarly journals Local Logics for Traces

2000 ◽  
Vol 7 (2) ◽  
Author(s):  
Igor Walukiewicz
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Dependence Graph ◽  
Graph Representation ◽  
Satisfiability Problem ◽  
Dependence Graphs ◽  
Local Logics

A mu-calculus over dependence graph representation of traces<br />is considered. It is shown that the mu-calculus cannot express all<br />monadic second order (MSO) properties of dependence graphs.<br />Several extensions of the mu-calculus are presented and it is proved<br />that these extensions are equivalent in expressive power to MSO<br />logic. The satisfiability problem for these extensions is PSPACE<br />complete.

Second-order logic, philosophical issues in

2018 ◽  
Author(s):  
Stewart Shapiro
Keyword(s):  
Mathematical Practice ◽  
Expressive Power ◽  
Deductive System ◽  
Second Order ◽  
Order Logic ◽  
Mathematical Structures ◽  
First Order ◽  
Correct Reasoning ◽  
Second Order Logic

Typically, a formal language has variables that range over a collection of objects, or domain of discourse. A language is ‘second-order’ if it has, in addition, variables that range over sets, functions, properties or relations on the domain of discourse. A language is third-order if it has variables ranging over sets of sets, or functions on relations, and so on. A language is higher-order if it is at least second-order. Second-order languages enjoy a greater expressive power than first-order languages. For example, a set S of sentences is said to be categorical if any two models satisfying S are isomorphic, that is, have the same structure. There are second-order, categorical characterizations of important mathematical structures, including the natural numbers, the real numbers and Euclidean space. It is a consequence of the Löwenheim–Skolem theorems that there is no first-order categorical characterization of any infinite structure. There are also a number of central mathematical notions, such as finitude, countability, minimal closure and well-foundedness, which can be characterized with formulas of second-order languages, but cannot be characterized in first-order languages. Some philosophers argue that second-order logic is not logic. Properties and relations are too obscure for rigorous foundational study, while sets and functions are in the purview of mathematics, not logic; logic should not have an ontology of its own. Other writers disqualify second-order logic because its consequence relation is not effective – there is no recursively enumerable, sound and complete deductive system for second-order logic. The deeper issues underlying the dispute concern the goals and purposes of logical theory. If a logic is to be a calculus, an effective canon of inference, then second-order logic is beyond the pale. If, on the other hand, one aims to codify a standard to which correct reasoning must adhere, and to characterize the descriptive and communicative abilities of informal mathematical practice, then perhaps there is room for second-order logic.

scholarly journals First order quantifiers in monadic second order logic

2004 ◽  
Vol 69 (1) ◽  
pp. 118-136 ◽  
Author(s):  
H. Jerome Keisler ◽  
Wafik Boulos Lotfallah
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
Existential Quantifier ◽  
Reachability Problem ◽  
Open Problems ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic ◽  
Quantifier Alternation

AbstractThis paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01].We introduce an operation existsn (S) on properties S that says “there are n components having S”. We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a corollary, if the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict.We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W.We introduce another operation alt(S) on properties which has the same relationship with the Circuit Value Problem as reach(S) (defined in [JM01]) has with the Directed Reachability Problem. We use alt(S) to show that Πn ⊈ FO(Σn), Σn ⊈ FO(∆n). and ∆n+1 ⊈ FOB(Σn), solving some open problems raised in [Mat98].

Complexity and expressive power of second-order extended Horn logic

2013 ◽  
Vol 59 (1-2) ◽  
pp. 4-11
Author(s):  
Shiguang Feng ◽  
Xishun Zhao
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Horn Logic

scholarly journals An approximative inference method for solving ∃∀SO satisfiability problems

2012 ◽  
Vol 45 ◽  
pp. 79-124 ◽  
Author(s):  
H. Vlaeminck ◽  
J. Vennekens ◽  
M. Denecker ◽  
M. Bruynooghe
Keyword(s):  
Constraint Propagation ◽  
Second Order ◽  
Order Logic ◽  
Satisfiability Problem ◽  
Finite Domain ◽  
Satisfiability Problems ◽  
Conformant Planning ◽  
Inductive Definitions ◽  
Powerful Knowledge ◽  
Second Order Logic

This paper considers the fragment ∃∀SO of second-order logic. Many interesting problems, such as conformant planning, can be naturally expressed as finite domain satisfiability problems of this logic. Such satisfiability problems are computationally hard (ΣP2) and many of these problems are often solved approximately. In this paper, we develop a general approximative method, i.e., a sound but incomplete method, for solving ∃∀SO satisfiability problems. We use a syntactic representation of a constraint propagation method for first-order logic to transform such an ∃∀SO satisfiability problem to an ∃SO(ID) satisfiability problem (second-order logic, extended with inductive definitions). The finite domain satisfiability problem for the latter language is in NP and can be handled by several existing solvers. Inductive definitions are a powerful knowledge representation tool, and this moti- vates us to also approximate ∃∀SO(ID) problems. In order to do this, we first show how to perform propagation on such inductive definitions. Next, we use this to approximate ∃∀SO(ID) satisfiability problems. All this provides a general theoretical framework for a number of approximative methods in the literature. Moreover, we also show how we can use this framework for solving practical useful problems, such as conformant planning, in an effective way.

scholarly journals Logics with Multiteam Semantics

2022 ◽  
Vol 23 (2) ◽  
pp. 1-30
Author(s):  
Erich Grädel ◽  
Richard Wilke
Keyword(s):  
Wide Spectrum ◽  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
Specific Class ◽  
Mathematical Basis ◽  
Logical Operators ◽  
Team Semantics ◽  
Independence Properties ◽  
Second Order Logic

Team semantics is the mathematical basis of modern logics of dependence and independence. In contrast to classical Tarski semantics, a formula is evaluated not for a single assignment of values to the free variables, but on a set of such assignments, called a team. Team semantics is appropriate for a purely logical understanding of dependency notions, where only the presence or absence of data matters, but being based on sets, it does not take into account multiple occurrences of data values. It is therefore insufficient in scenarios where such multiplicities matter, in particular for reasoning about probabilities and statistical independencies. Therefore, an extension from teams to multiteams (i.e. multisets of assignments) has been proposed by several authors. In this paper we aim at a systematic development of logics of dependence and independence based on multiteam semantics. We study atomic dependency properties of finite multiteams and discuss the appropriate meaning of logical operators to extend the atomic dependencies to full-fledged logics for reasoning about dependence properties in a multiteam setting. We explore properties and expressive power of a wide spectrum of different multiteam logics and compare them to second-order logic and to logics with team semantics. In many cases the results resemble what is known in team semantics, but there are also interesting differences. While in team semantics, the combination of inclusion and exclusion dependencies leads to a logic with the full power of both independence logic and existential second-order logic, independence properties of multiteams are not definable by any combination of properties that are downwards closed or union closed and thus are strictly more powerful than inclusion-exclusion logic. We also study the relationship of logics with multiteam semantics with existential second-order logic for a specific class of metafinite structures. It turns out that inclusion-exclusion logic can be characterised in a precise sense by the Presburger fragment of this logic, but for capturing independence, we need to go beyond it and add some form of multiplication. Finally, we also consider multiteams with weights in the reals and study the expressive power of formulae by means of topological properties.

scholarly journals Local Normal Forms for First-Order Logic with Applications to Games and Automata

1999 ◽  
Vol Vol. 3 no. 3 ◽  
Author(s):  
Thomas Schwentick ◽  
Klaus Barthelmann
Keyword(s):  
Normal Forms ◽  
Winning Strategy ◽  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Relational Structures ◽  
Second Order Logic ◽  
Monadic Second Order Logic

International audience Building on work of Gaifman [Gai82] it is shown that every first-order formula is logically equivalent to a formula of the form ∃ x_1,...,x_l, \forall y, φ where φ is r-local around y, i.e. quantification in φ is restricted to elements of the universe of distance at most r from y. \par From this and related normal forms, variants of the Ehrenfeucht game for first-order and existential monadic second-order logic are developed that restrict the possible strategies for the spoiler, one of the two players. This makes proofs of the existence of a winning strategy for the duplicator, the other player, easier and can thus simplify inexpressibility proofs. \par As another application, automata models are defined that have, on arbitrary classes of relational structures, exactly the expressive power of first-order logic and existential monadic second-order logic, respectively.

scholarly journals On Representations of Intended Structures in Foundational Theories

2021 ◽  
Author(s):  
Neil Barton ◽  
Moritz Müller ◽  
Mihai Prunescu
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
Trade Off ◽  
First Order ◽  
Informal Mathematics ◽  
Second Order Logic

AbstractOften philosophers, logicians, and mathematicians employ a notion of intended structure when talking about a branch of mathematics. In addition, we know that there are foundational mathematical theories that can find representatives for the objects of informal mathematics. In this paper, we examine how faithfully foundational theories can represent intended structures, and show that this question is closely linked to the decidability of the theory of the intended structure. We argue that this sheds light on the trade-off between expressive power and meta-theoretic properties when comparing first-order and second-order logic.

Study on Digital Content Representation from Direct Label Graph to RDF/OWL Language into Semantic Web

2014 ◽  
Vol 644-650 ◽  
pp. 3304-3309
Author(s):  
Khamis Abdul Latif Khamis ◽  
Luo Zhong ◽  
Hua Zhu Song
Keyword(s):  
Semantic Web ◽  
Expressive Power ◽  
Graph Representation ◽  
Label Graph ◽  
Object Class ◽  
Heritage Sites ◽  
Media Companies ◽  
Rdf Graph ◽  
Media Data ◽  
Direct Label

An increasing number of publication and consumptions of media data on the social and dynamic web has allowed ontology technology to grow up unpredictable. News agencies, cultural heritage sites, social media companies and ordinary users contribute a large portion of media contents across web community. These huge amounts of media contents are generally accessed via standardized and proprietary metadata formats through semantic web. But nearly all cases need specific, standardized, and more expressive methods to represent media data into the knowledge representation paradigm. This paper proposes the proper methods to express media ontology based on the nature of media data. At first RDF graph representation model is used to show the expressive power of domain classification with direct label graph concepts. Secondly, events and object class domain are used to express relational properties of media content. Finally, the events and object class domain is expressed into RDF/OWL language, as preferable and standardized language to represent media data in the semantic web.

Sign in / Sign up

Export Citation Format

Share Document