Search

We characterize non-distributive positive logic as the fragment of a single-sorted first-order language that is preserved by a new notion of simulation called a meet-simulation. Meet-simulations distinguish themselves from simulations because they relate pairs of states from one model to single states from another. En route to this result, we use a more traditional notion of simulations and prove a Hennessy–Milner-style theorem for it, using an analogue of modal saturation called meet-compactness. [ABSTRACT FROM AUTHOR]

Default Logics are a family of non-monotonic formalisms having so-called defaults and extensions as their common foundation. Traditionally, default logics have been defined and dealt with via syntactic notions of consequence in propositional or first-order logic. Here, we build default logics on modal logics. First, we present these default logics syntactically. Then, we elaborate on an algebraic counterpart. More precisely, we extend the notion of a modal algebra to accommodate for defaults and extensions. Our algebraic view of default logics concludes with an algebraic completeness result and a way of comparing default logics borrowing ideas from the concept of bisimulation in modal logic. To our knowledge, this take on default logics approach is novel. Interestingly, it also lays the groundwork for studying default logics from a dynamic logic perspective. [ABSTRACT FROM AUTHOR]

We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry 'First-Order Logic According to Fitting' by Berghofer in the Archive of Formal Proofs. The calculi and proof techniques are taken from Ben-Ari's textbook Mathematical Logic for Computer Science (Springer, 2012). We thereby demonstrate that Berghofer's approach works not only for natural deduction but also constitutes a framework for mechanically checked completeness proofs for a range of proof systems. [ABSTRACT FROM AUTHOR]

We extend classical first-order logic with a family of weak probability quantifiers, which we call submeasure quantifiers. Formulas are finitary, but infinitary deduction rules are needed. We consider first-order structures that are equipped with a countable family of submeasures (hence the name of the new quantifiers). We prove that every consistent set of sentences in the resulting logic is satisfiable in some structure as above. Then we restrict the set of formulas by requiring that no submeasure quantifier occurs within the scope of some classical quantifier. By suitably extending the deduction rules, we prove that every consistent set of sentences from the restricted class of formulas is satisfiable in some structure whose submeasures are actually outer measures. To perform the last step, we apply nonstandard techniques à la A. Robinson. [ABSTRACT FROM AUTHOR]

We study propositional and first-order Gödel logics over infinitary languages, which are motivated semantically by corresponding interpretations into the unit interval |$[0,1]$|⁠. We provide infinitary Hilbert-style calculi for the particular (propositional and first-order) cases with con-/disjunctions of countable length and prove corresponding completeness theorems by extending the usual Lindenbaum–Tarski construction to the infinitary case for a respective algebraic semantics via complete linear Heyting algebras. We provide infinitary hypersequent calculi and prove corresponding cut-elimination theorems in the Schütte–Tait style. Initial observations are made regarding truth-value sets other than |$[0,1]$|⁠. [ABSTRACT FROM AUTHOR]

Recent compositionality results in logic have highlighted the advantages of enlarging the traditional notion of logical matrix semantics, namely by incorporating non-determinism and partiality. Still, several important properties which are known to be computable for finite logical matrices have not been studied in the wider context of partial non-deterministic matrices (PNmatrices). In this paper, we study how incorporating non-determinism and/or partiality in logical matrices impacts on the computational properties of some natural problems regarding their induced logics and concretely their sets of theorems. We show that, while for some of these problems there is no relevant computational impact, there are problems whose computational complexity increases and still other problems that simply become undecidable. In particular, we show that the problem of checking whether the logics characterized by two finite PNmatrices have the same set of theorems is not decidable. This undecidability result explores the connection between PNmatrices and term-DAG-automata, where the universality problem is known to be undecidable. This link also motivates a final contribution, in the form of a pumping-like lemma, which can be used, in some cases, to show that a given logic cannot be characterized by a finite PNmatrix. [ABSTRACT FROM AUTHOR]

We explore two ways of formalizing Kreisel's addendum to the Brouwer–Heyting–Kolmogorov interpretation. To do this, we compare Artemov's justification logic with simply typed |$\lambda $| calculus. First, we provide a completeness result for Kripke style semantics of the implicational fragment of the intuitionistic logic of proofs. Then we introduce a map from justification terms into |$\lambda $| terms, which can be viewed as a method of extracting the computational content of the justification terms. Then we examine the interpretation of Kreisel's addendum in justification logic along with the image of the resulting justification terms under our map. [ABSTRACT FROM AUTHOR]

One-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential (universal) quantifiers that leave at most one variable free. We investigate this fragment over words and trees, presenting a complete classification of the complexity of its satisfiability problem for various navigational signatures and comparing its expressive power with other important formalisms. These include the two-variable fragment with counting and the unary negation fragment. [ABSTRACT FROM AUTHOR]

Lindström's theorem characterizes first-order logic in terms of its essential model theoretic properties. One cannot gain expressive power extending first-order logic without losing at least one of compactness or downward Löwenheim–Skolem property. We cast this result in an abstract framework of institution theory, which does not assume any internal structure either for sentences or for models, so it is more general than the notion of abstract logic usually used in proofs of Lindström's theorem; indeed, it can be said that institutional model theory is both syntax and semantics free. Our approach takes advantage of the methods of institutional model theory to provide a structured proof of Lindström's theorem at a level of abstraction applicable to any logical system that is strong enough to describe its own concept of isomorphism and its own concept of elementary equivalence. We apply our results to some logical systems formalized as institutions and widely used in computer science practice. [ABSTRACT FROM AUTHOR]

The rehabilitation scheduling process consists of planning rehabilitation physiotherapy sessions for patients, by assigning proper operators to them in a certain time slot of a given day, taking into account several requirements and optimizations. With the help of a smart application, which links wearable devices with the power of intelligent agents and complex event processing, patients are constantly and actively supervised during their daily activities. The paper I Incrementally predictive runtime verification i , by Angelo Ferrando and Giorgio Delzanno, discusses a lightweight formal verification technique used to verify the runtime behavior of software or hardware systems. [Extracted from the article]

Predicate intuitionistic logic is a well-established fragment of dependent types. Proof construction in this logic, as the Curry–Howard isomorphism states, is the process of program synthesis. We present automata that can handle proof construction and program synthesis in full intuitionistic first-order logic. Given a formula, we can construct an automaton such that the formula is provable if and only if the automaton has an accepting run. As further research, this construction makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections with the traditional logical connectives. [ABSTRACT FROM AUTHOR]

In the style of Lindström's theorem for classical first-order logic, this article characterizes propositional bi-intuitionistic logic as the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property and preservation under bi-asimulations. Since bi-intuitionistic logic introduces new complexities in the intuitionistic setting by adding the analogue of a backwards looking modality, the present paper constitutes a non-trivial modification of the previous work done by the authors for intuitionistic logic (Badia and Olkhovikov, 2020, Notre Dame Journal of Formal Logic , 61, 11–30). [ABSTRACT FROM AUTHOR]

In this paper, we present a first-order and a propositional logic for reasoning about degrees of confirmation. We define the appropriate formal languages and describe the corresponding classes of models. We provide infinitary axiomatizations for both logics and we prove that the axiomatizations are sound and strongly complete. We also show that our propositional logic is decidable. For some restrictions of the logics, we provide finitary axiomatic systems. [ABSTRACT FROM AUTHOR]

Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses , which are clauses that have a single literal. The second approach is partial regularization , which removes an inference |$\eta $| when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from |$\eta $| to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011 , p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included. [ABSTRACT FROM AUTHOR]

Modern logics of dependence and independence are based on team semantics, which means that formulae are evaluated not on a single assignment of values to variables, but on a set of such assignments, called a team. This leads to high expressive power, on the level of existential second-order logic. As an alternative, Baltag and van Benthem have proposed a local variant of dependence logic, called logic of functional dependence (⁠|$ {\textsf {LFD}}$|⁠). While its semantics is also based on a team, the formulae are evaluated locally on just one of its assignments, and the team just serves as the supply of the possible assignments that are taken into account in the evaluation process. This logic thus relies on the modal perspective of generalized assignments semantics and can be seen as a fragment of first-order logic. For the variant of |$ {\textsf {LFD}}$| without equality, the satisfiability problem is decidable. We extend the idea of localizing logics of dependence and independence in a systematic way, taking into account local variants of standard atomic dependency properties: besides dependence and independence, also inclusion, exclusion and anonymity. We study model-theoretic and algorithmic questions of the localized logics and also resolve some of the questions that had been left open by Baltag and van Benthem. In particular, we study decidability issues of the local logics and prove that satisfiability of |$ {\textsf {LFD}}$| with equality is undecidable. Further, we establish characterization theorems via appropriate notions of bisimulation and study the complexity of model checking problems for these logics. [ABSTRACT FROM AUTHOR]

We study the algorithmic properties of first-order monomodal logics of frames |$\langle {\textrm{I}\!\textrm{N}}, \leqslant \rangle $|⁠ , |$\langle {\textrm{I}\!\textrm{N}}, < \rangle $|⁠ , |$\langle \mathbb {Q}, \leqslant \rangle $|⁠ , |$\langle \mathbb {Q}, < \rangle $|⁠ , |$\langle {\textrm{I}\!\textrm{R}}, \leqslant \rangle $|⁠ , |$\langle {\textrm{I}\!\textrm{R}}, < \rangle $|⁠ , as well as some related logics, in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We show that the logics of frames based on |$ {\textrm{I}\!\textrm{N}}$| are |$\varPi ^1_1$| -hard—thus, not recursively enumerable—in languages with two individual variables, one monadic predicate letter and one proposition letter. We also show that the logics of frames based on |$\mathbb {Q}$| and |${\textrm{I}\!\textrm{R}}$| are |$\varSigma ^0_1$| -hard in languages with the same restrictions. Similar results are obtained for a number of related logics. [ABSTRACT FROM AUTHOR]

We consider the effect of restricting the number of individual variables, as well as the number and arity of predicate letters, in languages of first-order predicate superintuitionistic logics of finite Kripke frames on the logics' algorithmic properties. By a finite frame we mean a frame with a finite set of possible worlds. The languages we consider have no constants, function symbols or the equality symbol. We show that positive fragments of many predicate superintuitionistic logics of natural classes of finite Kripke frames are not recursively enumerable—more precisely, |$\varPi ^0_1$| -hard—in languages with three individual variables and a single monadic predicate letter; this applies to the logics of finite frames of the predicate counterparts of propositional logics lying between the intuitionistic logic and the logic of the weak law of the excluded middle. [ABSTRACT FROM AUTHOR]

We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov's Principle and Weak K̋nig's Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper. [ABSTRACT FROM AUTHOR]

This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting's nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic's semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic's semantics. [ABSTRACT FROM AUTHOR]

The reduction of undecidable first-order logic to decidable propositional logic via Herbrand's theorem has long been of interest to theoretical computer science, with the notion of a Herbrand proof motivating the definition of expansion proofs. In this paper we construct simple deep inference systems for first-order logic, both with and without cut, such that 'decomposed' proofs—proofs where the contractive and non-contractive behaviour of the proof is separated—in each system correspond to either expansion proofs or Herbrand proofs. Translations between proofs in this system, expansion proofs and Herbrand proofs are given, retaining much of the structure in each direction. [ABSTRACT FROM AUTHOR]

Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define Polyteam Semantics in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatization for the associated implication problem. We relate polyteam semantics to team semantics and investigate in which cases logics over the former can be simulated by logics over the latter. We also characterize the expressive power of poly-dependence logic by properties of polyteams that are downwards closed and definable in existential second-order logic (⁠|$\textsf{ESO}$|⁠). The analogous result is shown to hold for poly-independence logic and all |$\textsf{ESO}$| -definable properties. We also relate poly-inclusion logic to greatest fixed point logic. [ABSTRACT FROM AUTHOR]

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 [ABSTRACT FROM AUTHOR]

We generalize the characterization of elementary equivalence by Ehrenfeucht–Fraïssé games to arbitrary institutions whose sentences are finitary. These include many-sorted first-order logic, higher-order logic with types, as well as a number of other logics arising in connection to specification languages. The gain for the classical case is that the characterization is proved directly for all signatures, including infinite ones. [ABSTRACT FROM AUTHOR]

We study the effect of restricting the number of individual variables, as well as the number and arity of predicate letters, in languages of first-order predicate modal logics of finite Kripke frames on the logics' algorithmic properties. A finite frame is a frame with a finite set of possible worlds. The languages we consider have no constants, function symbols or the equality symbol. We show that most predicate modal logics of natural classes of finite Kripke frames are not recursively enumerable—more precisely, |$\varPi ^0_1$| -hard—in languages with three individual variables and a single monadic predicate letter. This applies to the logics of finite frames of the predicate extensions of the sublogics of propositional modal logics |$\textbf{GL}$|⁠ , |$\textbf{Grz}$| and |$\textbf{KTB}$| —among them, |$\textbf{K}$|⁠ , |$\textbf{T}$|⁠ , |$\textbf{D}$|⁠ , |$\textbf{KB}$|⁠ , |$\textbf{K4}$| and |$\textbf{S4}$|⁠. [ABSTRACT FROM AUTHOR]

In this article, we start with a two-player game that models communication under adverse circumstances in everyday life and study it from the perspective of a modal logic of graphs, where links can be deleted locally according to definitions available to the adversarial player. We first introduce a new language, semantics and some typical validities. We then formulate a new type of first-order translation for this modal logic and prove its correctness. Then, a novel notion of bisimulation is proposed that leads to a characterization theorem for the logic as a fragment of first-order logic, and a further investigation is made of its expressive power against hybrid modal languages. Next, we discuss how to axiomatize this logic of link deletion, using dynamic-epistemic logics as a contrast. Finally, we show that our new modal logic lacks both the tree model property and the finite model property and that its satisfiability problem is undecidable. [ABSTRACT FROM AUTHOR]

Justification logic is a term used to identify a relatively new family of modal-like logics. There is an established literature about propositional justification logic, but incursions on the first-order case are scarce. In this paper we present a constant domain semantics for the first-order logic of proofs with the Barcan Formula (FOLPb); then we prove Soundness and Completeness Theorems. A monotonic semantics for a version of this logic without the Barcan Formula is already in the literature, but constant domains require substantial new machinery, which may prove useful in other contexts as well. Although we work mainly with one system, we also indicate how to generalize these results for the quantified version of JT45 , the justification counterpart of the modal logic S5. We believe our methods are more generally applicable, but initially examining specific cases should make the work easier to follow. [ABSTRACT FROM AUTHOR]

We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic |$\textrm{FO}$| and (basic) modal logic |$\textrm{ML}$|⁠. We also present a version of the game for the modal |$\mu $| -calculus |$\textrm{L}_\mu $| and show that |$\textrm{FO}$| is also non-elementarily more succinct than |$\textrm{L}_\mu $|⁠. [ABSTRACT FROM AUTHOR]

We consider the hardness of approximation of optimization problems from the point of view of definability. For many |$\textrm{NP}$| -hard optimization problems it is known that, unless |$\textrm{P} = \textrm{NP} $|⁠ , no polynomial-time algorithm can give an approximate solution guaranteed to be within a fixed constant factor of the optimum. We show, in several such instances and without any complexity theoretic assumption, that no algorithm that is expressible in fixed-point logic with counting (FPC) can compute an approximate solution. Since important algorithmic techniques for approximation algorithms (such as linear or semidefinite programming) are expressible in FPC, this yields lower bounds on what can be achieved by such methods. The results are established by showing lower bounds on the number of variables required in first-order logic with counting to separate instances with a high optimum from those with a low optimum for fixed-size instances. [ABSTRACT FROM AUTHOR]

We study the satisfiability problem for two-variable first-order logic over structures with one transitive relation. We show that the problem is decidable in 2 -NExpTime for the fragment consisting of formulas where existential quantifiers are guarded by transitive atoms. As this fragment enjoys neither the finite model property nor the tree model property, to show decidability we introduce a novel model construction technique based on the infinite Ramsey theorem. We also point out why the technique is not sufficient to obtain decidability for the full two-variable logic with one transitive relation; hence, contrary to our previous claim, [FO |$^2$| with one transitive relation is decidable, STACS 2013: 317-328], the status of the latter problem remains open. [ABSTRACT FROM AUTHOR]

Formal ontologies are axiomatizations in a logic-based formalism. The development of formal ontologies is generating considerable research on the use of automated reasoning techniques and tools that help in ontology engineering. One of the main aims is to refine and to improve axiomatizations for enabling automated reasoning tools to efficiently infer reliable information. Defects in the axiomatization cannot only cause wrong inferences, but can also hinder the inference of expected information, either by increasing the computational cost of or even preventing the inference. In this paper, we introduce a novel, fully automatic white-box testing framework for first-order logic (FOL) ontologies. Our methodology is based on the detection of inference-based redundancies in the given axiomatization. The application of the proposed testing method is fully automatic since (i) the automated generation of tests is guided only by the syntax of axioms and (ii) the evaluation of tests is performed by automated theorem provers (ATPs). Our proposal enables the detection of defects and serves to certify the grade of suitability—for reasoning purposes—of every axiom. We formally define the set of tests that are (automatically) generated from any axiom and prove that every test is logically related to redundancies in the axiom from which the test has been generated. We have implemented our method and used this implementation to automatically detect several non-trivial defects that were hidden in various FOL ontologies. Throughout the paper we provide illustrative examples of these defects, explain how they were found and how each proof—given by an ATP—provides useful hints on the nature of each defect. Additionally, by correcting all the detected defects, we have obtained an improved version of one of the tested ontologies: Adimen-SUMO. [ABSTRACT FROM AUTHOR]

In this article we define pure intuitionistic Ancestral Logic (i A L), extending pure intuitionistic First-Order Logic (i F O L). This logic is a dependently typed abstract programming language with computational functionality beyond i F O L given by its realizer for the transitive closure, TC. We derive this operator from the natural type theoretic definition of TC using intersection. We show that provable formulas in i A L are uniformly realizable, thus i A L is sound with respect to constructive type theory. We further show that i A L subsumes Kleene Algebras with tests and thus serves as a natural programming logic for proving properties of program schemes. We also extract schemes from proofs that i A L specifications are solvable. [ABSTRACT FROM AUTHOR]

The core of this article is the modal correspondence theory in the class of all Euclidean frames. It shows that with respect to the class of all Euclidean frames, every modal formula is first-order definable and the problem of deciding the modal definability of sentences is undecidable. [ABSTRACT FROM AUTHOR]

The present article describes a method for proving Downward Löwenheim-Skolem Theorem within an arbitrary institution satisfying certain logic properties. In order to demonstrate the applicability of the present approach, the abstract results are instantiated to many-sorted first-order logic and preorder algebra. In addition to the first technique for proving Downward Löwenheim-Skolem Theorem, another one is developed, in the spirit of institution-independent model theory, which consists of borrowing the result from a simpler institution across an institution comorphism. As a result, the Downward Löwenheim-Skolem Property is exported from first-order logic to partial algebras, and from higher-order logic with intensional Henkin semantics to higher-order logic with extensional Henkin semantics. The second method successfully extends the domain of application of Downward Löwenheim-Skolem Theorem to other non-conventional logical systems for which the first technique may fail. One major application of Downward Löwenheim-Skolem Theorem is interpolation in constructor-based logics with universally quantified sentences. The interpolation property is established by borrowing it from a base institution for its constructor-based variant across an institution morphism. This result is important as interpolation for constructor-based first-order logics is still an open problem. [ABSTRACT FROM AUTHOR]

The core of our article is the computability of the problem of deciding the modal definability of first-order sentences with respect to classes of frames. It gives a new proof of Chagrova's Theorem telling that, with respect to the class of all frames, the problem of deciding the modal definability of first-order sentences is undecidable. It also gives the proofs of new variants of Chagrova's Theorem. [ABSTRACT FROM AUTHOR]

Coalgebraic modal logic serves as a unifying framework to study a wide range of modal logics beyond the relational realm, including probabilistic and graded logics as well as conditional logics and logics based on neighbourhoods and games. Coalgebraic predicate logic (CPL), a generalization of a neighbourhood-based first-order logic introduced by Chang, has been identified as a natural first-order extension of coalgebraic modal logic, which in particular coincides with the standard first-order correspondence language when instantiated to Kripke-style relational modal operators. Here, we generalize to the CPL setting the classical van Benthem/Rosen theorem stating that both over arbitrary and over finite models, modal logic is precisely the bisimulation-invariant fragment of first-order logic. As instances of this generic result, we obtain corresponding characterizations for, e.g. conditional logic, neighbourhood logic (i.e. classical modal logic) and monotone modal logic. [ABSTRACT FROM AUTHOR]

BDI (Bounded Depth Increase) is a new decidable first-order clause class. It strictly includes known classes such as PVD. The arity of function and predicate symbols as well as the shape of atoms is not restricted in BDI. Instead the shape of 'cycles' in resolution inferences is restricted so that the depth of generated clauses may increase but is still finitely bound. The BDI class is motivated by real-world problems where function terms are used to represent record structures. We show that the hyper-resolution calculus modulo redundancy elimination terminates on BDI clause sets. Employing this result to the ordered resolution calculus, we can also prove termination of ordered resolution on BDI, yielding a more efficient decision procedure. [ABSTRACT FROM AUTHOR]

In this article, we present an efficient construction of the Game Description Language (GDL) interpreter. GDL is a first-order logic language used in the General Game Playing (GGP) framework. Syntactically, the language is a subset of Datalog and Prolog, and like those two, is based on facts and rules. Our aim was to achieve higher execution speed than anyone's of the currently available tools, including other Prolog interpreters applied to GDL. Speed is a crucial factor of the state space search methods used by most GGP agents, since the faster the GDL reasoner, the more game states can be evaluated in the allotted time. The cornerstone of our interpreter is the resolution tree which reflects the dependencies between rules. Our paradigm was to expedite any heavy workload to the preprocessing step to optimize the real-time usage. The proposed enhancements effectively maintain a balance between the time needed to build the internal data representation and the time required for data analysis during actual play. Therefore we refrain from using tree-based dictionary approaches such as TRIE to store the results of logical queries in favour of a memory-friendly linear representation and dynamic filters to reduce space complexity. Experimental results show that our interpreter outperforms the two most popular Prolog interpreters used by GGP programs: Yet Another Prolog (YAP) and ECLiPSe, respectively, in 22 and 26 games, out of the 28 tested. We give some insights into possible reasons for the edge of our approach over Prolog. [ABSTRACT FROM AUTHOR]

We introduce a first sequent-style calculus for witnessed Gödel logic. Our calculus makes use of the cut rule. We show that this is inescapable by establishing a general result on the non-existence of suitable analytic calculi for a large class of first-order logics. These include witnessed Gödel logic, (fragments of) Łukasiewicz logic and intuitionistic logic extended with the quantifiers of classical logic. [ABSTRACT FROM AUTHOR]

The standard first-order reading of modality does not bind individual variables, i.e. if x is free in F(x), then x remains free in F(x). Accordingly, if stands for 'provable in arithmetic,' ∀x F(x) states that F(n) is provable for any given value of n=0,1,2,...; this corresponds to a de re reading of modality. The other, de dicto meaning of F(x), suggesting that F(x) is derivable as a formula with a free variable x, is not directly represented by a modality, though, semantically, it could be approximated by compound constructions, e.g. ∀xF(x). We introduce the first-order logic FOS4* in which modalities can bind individual variables and, in particular, can directly represent both de re and de dicto modalities. FOS4* extends first-order S4 and is the natural forgetful projection of the first-order logic of proofs FOLP. The same method of introducing binding modalities obviously works for other modal logics as well. [ABSTRACT FROM AUTHOR]

We consider intermediate predicate logics defined by fixed well-ordered (or dually well-ordered) linear Kripke frames with constant domains where the order-type of the well-order is strictly smaller than ωω. We show that two such logics of different order-type are separated by a first-order sentence using only one monadic predicate symbol. Previous results by Minari, Takano and Ono, as well as the second author, obtained the same separation but relied on the use of predicate symbols of unbounded arity. [ABSTRACT FROM AUTHOR]

The article introduces notions of first-order asimulation and first-order k-asimulation, which extend notions of asimulation and k-asimulation introduced in Olkhovikov (2012, Review of Symbolic Logic, 6, 348–365) onto the level of intuitionistic predicate logic. We then prove that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula iff it is invariant with respect to first-order k-asimulations for some k, and then that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula iff it is invariant with respect to first-order asimulations. Finally, it is proved that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula over a class of intuitionistic models (intuitionistic models with constant domain) iff it is invariant with respect to first-order asimulations between intuitionistic models (intuitionistic models with constant domain). [ABSTRACT FROM PUBLISHER]

We show that the first-order theories of the s-degrees, and of the Q-degrees, are computably isomorphic to true second-order arithmetic. [ABSTRACT FROM PUBLISHER]

Let Γ be a (not necessarily finite) structure with a finite relational signature. We prove that deciding whether a given existential positive sentence holds in Γ is in LogSpace or complete for the class CSP(Γ)NP under deterministic polynomial-time many-one reductions. Here, CSP(Γ)NP is the class of problems that can be reduced to the constraint satisfaction problem of Γ under non-deterministic polynomial-time many-one reductions. [ABSTRACT FROM AUTHOR]

J. Raymundo Marcial–Romero and M. H. Escardó described a functional programming language with an abstract data type real for the real numbers and a non-deterministic operator rtest: real → bool. We show that this language is universal at first order, as conjectured by these authors: all computable, first-order total functions on the real numbers are definable. To be precise, we show that each computable function f: ℝ → ℝ we consider is the extension of the denotation 〚Mf〛 of some program Mf: real → real, in a model based on power domains, described in previous work. Whereas this semantics is only an approximate one, in the sense that programs may have a denotation strictly below their true outputs, our result shows that, to compute a given function, it is in fact always possible to find a program with a faithful denotation. We briefly indicate how our proof extends to show that functions taken from a large class of computable, first-order partial functions in several arguments are definable. [ABSTRACT FROM AUTHOR]

Kamp (PhD Thesis, University of California, LA) proved that the tense logic of the connectives Until and Since is expressively complete over the class DCLO of Dedekind complete linear orders in the sense that this logic can express exactly the same conditions over DCLO as first-order logic. In the present article a modification of the question of expressive completeness is considered—the question of whether there exists a basis consisting of a finite number of modal-logical connectives for monadic second-order logic. The notion of k-dimensional basis that Gabbay (1981, Aspects of Philosophical Logic, 91–117) defined relative to FO is generalized to arbitrary abstract logics, and it is shown that a finite 2-dimensional basis exists for MSO on the class FLO of all finite linear structures. Beauquier and Rabinovich (2002, J. Logic. Comput., 12, 243–253) have proven that there is no finite 1-dimensional basis for MSO on FLO. Thus, the result yielding a 2-dimensional basis cannot be improved. [ABSTRACT FROM AUTHOR]

In most termination tools two ingredients, namely recursive path orderings (RPOs) and polynomial interpretation orderings (POLOs), are used in a consecutive disjoint way to solve the final constraints generated from the termination problem. In this article we present a simple ordering that combines both RPO and POLO and defines a family of orderings that includes both, and extend them with the possibility of having, at the same time, an RPO-like treatment for some symbols and a POLO-like treatment for the others. The ordering is extended to higher-order terms, providing a new fully automatable use of polynomial interpretations in combination with beta-reduction. [ABSTRACT FROM AUTHOR]

We provide a constructive direct semantic proof of the completeness of the cut-free part of the hypersequent calculus HIF for the standard first-order Gödel logic (thereby proving both completeness of the calculus for its standard semantics, and the admissibility of the cut rule in the full calculus). The results also apply to derivations from assumptions (or ‘non-logical axioms’), showing in particular that when the set of assumptions is closed under substitutions, then cuts can be confined to formulas occurring in the assumptions. The methods and results are then extended to handle the (Baaz) Delta connective as well. [ABSTRACT FROM AUTHOR]

Measuring inconsistency in knowledge bases has been recognized as an important problem in several research areas. Many methods have been proposed to solve this problem and a main class of them is based on some kind of paraconsistent semantics. However, existing methods suffer from two limitations: (i) they are mostly restricted to propositional knowledge bases; (ii) very few of them discuss computational aspects of computing inconsistency measures. In this article, we try to solve these two limitations by exploring algorithms for computing an inconsistency measure of first-order knowledge bases. After introducing a four-valued semantics for first-order logic, we define an inconsistency measure of a first-order knowledge base, which is a sequence of inconsistency degrees. We then propose a precise algorithm to compute our inconsistency measure. We show that this algorithm reduces the computation of the inconsistency measure to classical satisfiability checking. This is done by introducing a new semantics, named S[n]-4 semantics, which can be calculated by invoking a classical SAT solver. Moreover, we show that this auxiliary semantics also gives a direct way to compute upper and lower bounds of inconsistency degrees. That is, it can be easily revised to compute approximating inconsistency measures. The approximating inconsistency measures converge to the precise values if enough resources are available. Finally, by some nice properties of the S[n]-4 semantics, we show that some upper and lower bounds can be computed in P-time, which says that the problem of computing these approximating inconsistency measures is tractable. [ABSTRACT FROM PUBLISHER]

We show that for each n and m, there is an existential first order sentence that is NOT logically equivalent to a sentence of quantifier rank at most m in infinitary logic augmented with all generalized quantifiers of arity at most n. We use this to show the strictness of the quantifier rank hierarchies for various logics ranging from existential (or universal) fragments of first-order logic to infinitary logics augmented with arbitrary classes of generalized quantifiers of bounded arity.The sentence above is also shown to be equivalent to a first-order sentence with at most n+2 variables (free and bound). This gives the strictness of the quantifier rank hierarchies for various logics with only n+2 variables. The proofs use the bijective Ehrenfeucht–Fraïsse game and a modification of the building blocks of Hella. [ABSTRACT FROM PUBLISHER]

The completeness of the infinitary language ℒω1,ω was proved by Carol Karp in 1964.We express and prove the completeness of infinitary first-order logics in the institution-independent setting by using forcing, a powerful method for constructing models. As a consequence of this abstraction, the completeness theorem becomes available for the infinitary versions of many ‘first order’ logical systems that appear in the area of logic or computer science. [ABSTRACT FROM PUBLISHER]