Wyniki wyszukiwania - BazTech

1

A model theory for the potential infinite

Eberl Matthias

Reports on Mathematical Logic

|

2022

|

Vol. 57

3--29

EN

We present the model theoretic concepts that allow mathematics to be developed with the notion of the potential infinite instead of the actual infinite. The potential infinite is understood as a dynamic notion, being an indefinitely extensible finite. The main adoption is the interpretation of the universal quantifier, which has an implicit reflection principle. Each universal quantification refers to an indefinitely large, but finite set. The quantified sets may increase, so after a reference by quantification, a further reference typically uses a larger, still finite set. We present the concepts for classical first-order logic and show that these dynamic models are sound and complete with respect to the usual inference rules. Moreover, a finite set of formulas requires a finite part of the increasing model for a correct interpretation.

2

Reversible Regular Languages : Logical and Algebraic Characterisations

Gastin Paul, Manuel Amaldev, Govind R.

Fundamenta Informaticae

|

2021

|

Vol. 180, nr 4

333--350

EN

We present first-order (FO) and monadic second-order (MSO) logics with predicates ‘between’ and ‘neighbour’ that characterise the class of regular languages that are closed under the reverse operation and its subclasses. The ternary between predicate bet(x, y, z) is true if the position y is strictly between the positions x and z. The binary neighbour predicate N(x, y) is true when the the positions x and y are adjacent. It is shown that the class of reversible regular languages is precisely the class definable in the logics MSO(bet) and MSO(N). Moreover the class is definable by their existential fragments EMSO(bet) and EMSO(N), yielding a normal form for MSO formulas. In the first-order case, the logic FO(bet) corresponds precisely to the class of reversible languages definable in FO(<). Every formula in FO(bet) is equivalent to one that uses at most 3 variables. However the logic FO(N) defines only a strict subset of reversible languages definable in FO(+1). A language-theoretic characterisation of the class of languages definable in FO(N), called locally-reversible threshold-testable (LRTT), is given. In the second part of the paper we show that the standard connections that exist between MSO and FO logics with order and successor predicates and varieties of finite semigroups extend to the new setting with the semigroups extended with an involution operation on its elements. The case is different for FO(N) where we show that one needs an additional equation that uses the involution operator to characterise the class. While the general problem of characterising FO(N) is open, an equational characterisation is shown for the case of neutral letter languages.

3

Complexity and (Un)decidability of Fragments of 〈ωωλ;×〉

Bès Alexis, Choffrut Christian

Fundamenta Informaticae

|

2019

|

Vol. 164, nr 1

1--15

EN

We specify the frontier of decidability for fragments of the first-order theory of ordinal multiplication. We give a NEXPTIME lower bound for the complexity of the existential fragment of 〈ωω λ; ×,ω,ω+1,ω2+1〉 for every ordinal λ. Moreover, we prove (by reduction from Hilbert Tenth Problem) that the ∃*∀6-fragment of 〈ωω λ; ×〉 is undecidable for every ordinal λ.

4

On Modalities and Quantifiers

Fitting M.

Fundamenta Informaticae

|

2017

|

Vol. 156, nr 3/4

297--330

EN

In 1951 in his book An Essay in Modal Logic, Georg Henrik von Wright strongly called attention to the analogies between quantifiers and modal operators. In 1984 I published a paper in Synthese examining the analogy formally. Confession: the presentation in that paper was badly done, and there is a significant (though correctable) error. Its time to repair the damage, present the ideas in a better way, and continue the investigation further. There are natural sublogics of classical first-order logic that are direct analogs of standard, basic modal logics. The behavior of quantifiers can be given a possible world semantics, some analogous to normal models, some to regular models, and some to neighborhood models. The firstorder logics have axiom systems and generally also tableau systems, paralleling those of modal logics. Many have the interpolation property. This gives concrete substance to von Wright’s observations. But then, what is the crucial difference between modal operators and quantifiers? This turns out to be surprising in its simplicity, and leads to an interesting way of looking at the familiar Henkin style completeness proof for first-order logic.

5

Forcing for First-Order Languages from the Perspective of Rasiowa-Sikorski Lemma

Czelakowski J.

Fundamenta Informaticae

|

2017

|

Vol. 156, nr 3/4

255--280

EN

The paper is concerned with the problem of building models for first-order languages from the perspective of the classic paper of Rasiowa and Sikorski [9]. The central idea, developed in this paper, consists in constructing first-order models from individual variables. The key notion of a Rasiowa–Sikorski set of formulas for an arbitrary countable language L is examined. Each Rasiowa–Sikorski set defines a countable model for L. Conversely, every countable model for L is determined by a Rasiowa-Sikorski set. The focus is on constructing Rasiowa-Sikorski sets by applying forcing techniques restricted to Boolean algebras arising from the subsets of the set of atomic formulas of L.

6

A Resolution Calculus for First-order Schemata

Aravantinos V., Echenim M., Peltier N.

Fundamenta Informaticae

|

2013

|

Vol. 125, nr 2

101--133

EN

We devise a resolution calculus that tests the satisfiability of infinite families of clause sets, called clause set schemata. For schemata of propositional clause sets, we prove that this calculus is sound, refutationally complete, and terminating. The calculus is extended to first-order clauses, for which termination is lost, since the satisfiability problem is not semi-decidable for nonpropositional schemata. The expressive power of the considered logic is strictly greater than the one considered in our previous work.

7

A Logic Framework for Incremental Learning of Process Models

Ferilli S., Esposito F.

Fundamenta Informaticae

|

2013

|

Vol. 128, nr 4

413--443

EN

Standardized processes are important for correctly carrying out activities in an organization. Often the procedures they describe are already in operation, and the need is to understand and formalize them in a model that can support their analysis, replication and enforcement. Manually building these models is complex, costly and error-prone. Hence, the interest in automatically learning them from examples of actual procedures. Desirable options are incrementality in learning and adapting the models, and the ability to express triggers and conditions on the tasks that make up the workflow. This paper proposes a framework based on First-Order Logic that solves many shortcomings of previous approaches to this problem in the literature, allowing to deal with complex domains in a powerful and flexible way. Indeed, First-Order Logic provides a single, comprehensive and expressive representation and manipulation environment for supporting all of the above requirements. A purposely devised experimental evaluation confirms the effectiveness and efficiency of the proposed solution.

8

A General Similarity Framework for Horn Clause Logic

Ferilli S., Basile T.M.A., Biba M., Di Mauro N., Esposito F.

Fundamenta Informaticae

|

2009

|

Vol. 90, nr 1-2

43-66

EN

First-Order Logic formulć are a powerful representation formalism characterized by the use of relations, that cause serious computational problems due to the phenomenon of indeterminacy (various portions of one description are possibly mapped in different ways onto another description). Being able to identify the correct corresponding parts of two descriptions would help to tackle the problem: hence, the need for a framework for the comparison and similarity assessment. This could have many applications in Artificial Intelligence: guiding subsumption procedures and theory revision systems, implementing flexible matching, supporting instance-based learning and conceptual clustering. Unfortunately, few works on this subject are available in the literature. This paper focuses on Horn clauses, which are the basis for the Logic Programming paradigm, and proposes a novel similarity formula and evaluation criteria for identifying the descriptions components that are more similar and hence more likely to correspond to each other, based only on their syntactic structure. Experiments on real-world datasets prove the effectiveness of the proposal, and the efficiency of the corresponding implementation in the above tasks.

9

Logical Undecidabilities Made Easy

Leivan D.

Fundamenta Informaticae

|

2008

|

Vol. 89, nr 2-3

307-312

EN

Referring to symbolic computing permits extremely simple proofs of undecidability for first-order logic and theories of basic structures. Using grammars we obtain a trivial proof that firstorder validity is undecidable (already for formulas with quantifier prefix ∃∃ and referring to only one unary relation and one binary function [2]). A similar proof yields Gödel's First Incompleteness Theorem for the structure of strings; undecidability for arithmetic follows by noting that addition and multiplication permit direct coding of string concatenation.

10

On First-Order Fragments for Mazurkiewicz Traces

Diekert V., Horsch M., Kufleitner M.

Fundamenta Informaticae

|

2007

|

Vol. 80, nr 1-3

1-29

EN

Mazurkiewicz traces form a model for concurrency. Temporal logic and first-order logic are important tools in order to deal with the abstract behavior of such systems. Since typical properties can be described by rather simple logical formulas one is interested in logical fragments. One focus of this paper is unary temporal logic and first-order logic in two variables. Over words, this corresponds to the variety of finite monoids called DA. However, over Mazurkiewicz traces it is crucial whether traces are given as dependence graphs or as partial orders (over words these notions coincide). The main technical contribution is a generalization of important characterizations of DA from words to dependence graphs, whereas the use of partial orders leads to strictly larger classes. As a consequence we can decide whether a first-order formula over dependence graphs is equivalent to a first-order formula in two variables. The corresponding result for partial orders is not known. This difference between dependence graphs and partial orders also affects the complexity of the satisfiability problems for the fragments under consideration: for first-order formulas in two variables we prove an NEXPTIME upper bound, whereas the corresponding problem for partial orders leads to EXPSPACE. Furthermore, we give several separation results for the alternation hierarchy for first-order logic. It turns out that even for those levels at which one can express the partial order relation in terms of dependence graphs, the fragments over partial orders have more expressive power.

11

Composition Theorem for Generalized Sum

Rabinovich A.

Fundamenta Informaticae

|

2007

|

Vol. 79, nr 1-2

137-167

EN

Composition theorems are tools which reduce sentences about some compound structure to sentences about its parts. A seminal example of such a theorem is the Feferman-Vaught Theorem [3] which reduces the first-order theory of generalized products to the first order theory of its factors and the monadic second-order theory of index structure. Shelah [23] used the composition theorem for linear orders as one of the main tools for obtaining very strong decidability results for the monadic second-order theory of linear orders. The main technical contribution of our paper is (1) a definition of a generalized sum of structures and (2) a composition theorem for first-order logic over the generalized sum. One of our objectives is to emphasize the work-out of the composition method.

12

Learning First-Order Rules: A Rough Set Approach

Stepaniuk J., Hońko P.

Fundamenta Informaticae

|

2004

|

Vol. 61, nr 2

139--157

EN

The aim of this paper is to introduce and investigate an algorithm RSRL for finding first-order logic rules. Rough set methodology is used in the process of selecting literals which may be a part of a rule. The criterion of selecting a literal is as follows: only such a literal is selected, which added to the rule makes the rule discerning the most examples which were indiscernible so far.

13

Constructing Decision Procedures in Equational Clausal Logic

Peltier N.

Fundamenta Informaticae

|

2003

|

Vol. 54, nr 1

17-65

EN

A method is proposed to construct decision procedures for various subclasses of first-order logic with equality. We define a notion of complexity of first-order terms and equations, and we propose semantic and syntactic criteria ensuring that existing refinements of the paramodulation calculus terminate on the considered clause sets. These refinements use reduction orderings, selection functions and simplification rules. Since they are sound and refutationally complete, the corresponding classes of formulae are decidable. Moreover, the automatic extraction of models from saturated clause sets is also possible. A discussion and detailed comparisons with existing works in the field are provided, together with numerous examples and some undecidability results.

14

An extended Relational Algebra on Abstract Objects for summarizing answers to queries

Demolombe R.

Fundamenta Informaticae

|

2003

|

Vol. 57, nr 1

1--15

EN

Answers to queries in terms of abstract objects are defined in the logical framework of first order predicate calculus. A partial algebraic characterisation of the supremum and of the infimum of abstract answers is given in an extended Relational Algebra of the Cylindric Algebra kind. Then, the form of queries is restricted in order to be able to compute answers without the cylindrification operator. For these restricted queries we give a technique to compute an upper bound and a lower bound of abstract answers using only the operators of the standard Relational Algebra.

15

A Logical Approach to Control. Some New Logical Concepts and their Application to the Notion of Safety for Control Variants

Terlikowski T.

Fundamenta Informaticae

|

2002

|

Vol. 52, nr 4

377-394

EN

In this paper, we introduce logical notions of positive implication and positive correspondence aimed at a formalization of notions of safety of control variants in control theory.

16

A model-theoretic version of the complement theorem : applications

Nowak K.

Bulletin of the Polish Academy of Sciences. Mathematics

|

1999

|

Vol. 47, no 4

355-361

EN

The paper treats of some consequences of the model-theoretic version of Gabrielov's complement theorem from [11], which asserts that the theories T[sub an] (introduced in [11] and T'[sub an] (defined herein) are model-complete. The theory T'[sub an] is a universal modification of T[sub an] in the language L'[sub an] of ordered rings expanded by the symbols of restricted analytic functions, arithmetic roots and multiplicative inverse l/x. We give a short proof of the curve selecting lemma, and next we demonstrate how quantifier elimination, within the structure R[sub an] expanded by multiplicative inverse 1/x (a result due to Denef-van den Dries [4], can be obtained from the complement theorem through a general method of logic. Also presented is an application to definability problems ; namely, a piecewise description of a subanalytic function by restricted analytic functions, arithmetic roots and l/x.

17

A model-theoretic version of the complement theorem

Nowak K.

Bulletin of the Polish Academy of Sciences. Mathematics

|

1999

|

Vol. 47, no 4

345-353

EN

This paper deals with an axiomatic theory T[sub an] and the expansion R[sub an] of the ordered field of reals, formed by attaching the restricted analytic functions. We show that the theory T[sub an] is model-complete, which may be regarded as a version of Gabrielov's complement theorem. Our proof is based on Robinson's test and it does not involve a partition technique. An immediate corollary is that T[sub an] coincides with the semantic theory Th(R[sub an]) of all sentences true in the structure R[sub an].

18

Automated deduction techniques for studying Rough Algebras

Vigneron L.

Fundamenta Informaticae

|

1998

|

Vol. 33, nr 1

85-103

EN

We present a non-exhaustive state of the art. In the domain of deduction in first-order logic with equality, describing different strategies introduced over the years: strategies for selecting deduction steps, for eliminating redundant information, for delaying the resolution of unsolved or too difficult problems, for applying deductions with built-in-properties. We also present the system dalac that implements our deduction techniques modulo associative-commutative properties. Finally we detail an application of those techniques to the study of non-classical logics, work realised in collaboration with Prof. Wasilewska (Stony Brook University, New York).