A NORMAL FORM FOR FIRST-ORDER LOGIC OVER DOUBLY-LINKED DATA STRUCTURES

2008 ◽  
Vol 19 (01) ◽  
pp. 205-217 ◽  
Author(s):  
STEVEN LINDELL
Keyword(s):  
Normal Form ◽  
Data Structures ◽  
Linked Data ◽  
Linear Time ◽  
Order Logic ◽  
Information Storage ◽  
First Order Logic ◽  
Total Size ◽  
Bounded Degree ◽  
First Order

We use singulary vocabularies to analyze first-order definability over doubly-linked data structures. Singulary vocabularies contain only monadic predicate and monadic function symbols. A class of mathematical structures in any vocabulary can be elementarily interpreted in a singulary vocabulary, while preserving notions of total size and degree. Doubly-linked data structures are a special case of bounded-degree finite structures in which there are reciprocal connections between elements, corresponding closely with physically feasible models of information storage. They can be associated with logical models involving unary relations and bijective functions in what we call an invertible singulary vocabulary. Over classes of these models, there is a normal form for first-order logic which eliminates all quantification of dependent variables. The paper provides a syntactically based proof using counting quantifiers. It also makes precise the notion of implicit calculability for arbitrary arity first-order formulas. Linear-time evaluation of first-order logic over doubly-linked data structures becomes a direct corollary. Included is a discussion of why these special data structures are appropriate for physically realizable models of information.

scholarly journals Simulating reachability using first-order logic with applications to verification of linked data structures

2009 ◽  
Vol 5 (2) ◽  
Author(s):  
Tal Lev-Ami ◽  
Neil Immerman ◽  
Thomas Reps ◽  
Mooly Sagiv ◽  
Siddharth Srivastava ◽  
...  
Keyword(s):  
Data Structures ◽  
Linked Data ◽  
Order Logic ◽  
First Order Logic ◽  
First Order

Linear time computable problems and first-order descriptions

1996 ◽  
Vol 6 (6) ◽  
pp. 505-526 ◽  
Author(s):  
Detlef Seese
Keyword(s):  
Mathematical Logic ◽  
Polynomial Time ◽  
Linear Time ◽  
Order Logic ◽  
First Order Logic ◽  
Algorithmic Problem ◽  
Bounded Degree ◽  
First Order ◽  
Relational Structures ◽  
Formal Theories

It is well known that every algorithmic problem definable by a formula of first-order logic can be solved in polynomial time, since all these problems are inL(see Aho and Ullman (1979) and Immerman (1987)). Using an old technique of Hanf (Hanf 1965) and other techniques developed to prove the decidability of formal theories in mathematical logic, it is shown that an arbitraryFO-problem over relational structures of bounded degree can be solved in linear time.

scholarly journals Extensions in graph normal form

2020 ◽  
Author(s):  
Michał Walicki
Keyword(s):  
Normal Form ◽  
Fixed Points ◽  
Propositional Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

Notions of locality and their logical characterizations over finite models

1999 ◽  
Vol 64 (4) ◽  
pp. 1751-1773 ◽  
Author(s):  
Lauri Hella ◽  
Leonid Libkin ◽  
Juha Nurmonen
Keyword(s):  
Small Degree ◽  
Order Logic ◽  
First Order Logic ◽  
Bounded Degree ◽  
First Order ◽  
Finite Models ◽  
Order Case ◽  
The Relationship

AbstractMany known tools for proving expressibility bounds for first-ordér logic are based on one of several locality properties. In this paper we characterize the relationship between those notions of locality. We note that Gaifman's locality theorem gives rise to two notions: one deals with sentences and one with open formulae. We prove that the former implies Hanf's notion of locality, which in turn implies Gaifman's locality for open formulae. Each of these implies the bounded degree property, which is one of the easiest tools for proving expressibility bounds. These results apply beyond the first-order case. We use them to derive expressibility bounds for first-order logic with unary quantifiers and counting. We also characterize the notions of locality on structures of small degree.

scholarly journals Successor-Invariant First-Order Logic on Classes of Bounded Degree (Extended Abstract)

2021 ◽  
Author(s):  
Julien Grange
Keyword(s):  
Expressive Power ◽  
Order Logic ◽  
First Order Logic ◽  
Bounded Degree ◽  
First Order ◽  
Successor Relation

We study the expressive power of successor-invariant first-order logic, which is an extension of first-order logic where the usage of a successor relation on the vertices of the graph is allowed, as long as the validity of formulas is independent on the choice of a particular successor. We show that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.

scholarly journals Question Answering over Linked Data Using First-order Logic

2014 ◽  
Author(s):  
Shizhu He ◽  
Kang Liu ◽  
Yuanzhe Zhang ◽  
Liheng Xu ◽  
Jun Zhao
Keyword(s):  
Linked Data ◽  
Question Answering ◽  
Order Logic ◽  
First Order Logic ◽  
First Order

RULES FOR SUBATOMIC DERIVATION

2010 ◽  
Vol 4 (2) ◽  
pp. 219-236 ◽  
Author(s):  
BARTOSZ WIĘCKOWSKI
Keyword(s):  
Normal Form ◽  
Atomic System ◽  
Atomic Level ◽  
Order Logic ◽  
First Order Logic ◽  
Atomic Sentence ◽  
Theoretic Analysis ◽  
Alternative Account ◽  
First Order ◽  
Normal Form Theorem

In proof-theoretic semantics the meaning of an atomic sentence is usually determined by a set of derivations in an atomic system which contain that sentence as a conclusion (see, in particular, Prawitz, 1971, 1973). The paper critically discusses this standard approach and suggests an alternative account which proceeds in terms of subatomic introduction and elimination rules for atomic sentences. A simple subatomic normal form theorem by which this account of the semantics of atomic sentences and the terms from which they are composed is underpinned, shows moreover that the proof-theoretic analysis of first-order logic can be pursued also beneath the atomic level.

Sign in / Sign up

Export Citation Format

Share Document