Related papers: First-order Logic as a Constraint Programming Lang…

In this paper we adapt the definitions and results from Apt and Vermeulen on `First order logic as a constraint programming language' (in: Proceedings of LPAR2001, Baaz and Voronkov (eds.), Springer LNAI 2514) to include important ideas…

In Apt and Bezem [AB99] (see cs.LO/9811017) we provided a computational interpretation of first-order formulas over arbitrary interpretations. Here we complement this work by introducing a denotational semantics for first-order logic.…

A policy describes the conditions under which an action is permitted or forbidden. We show that a fragment of (multi-sorted) first-order logic can be used to represent and reason about policies. Because we use first-order logic, policies…

We will investigate proof-theoretic and linguistic aspects of first-order linear logic. We will show that adding partial order constraints in such a way that each sequent defines a unique linear order on the antecedent formulas of a sequent…

Qualification has been recently introduced as a generalization of uncertainty in the field of Logic Programming. In this report we investigate a more expressive language for First-Order Functional Logic Programming with Constraints and…

Contemporary semantic description of logic is based on the ontology of all possible interpretations, an insufficiently clear metaphysical concept. In this article, logic is described as the internal organization of language. Logical…

We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formulas -- the precise subset of the universe upon which their…

Many logic programming based approaches can be used to describe and solve combinatorial search problems. On the one hand there is constraint logic programming which computes a solution as an answer substitution to a query containing the…

This paper deals with a problem from discrete-time robust control which requires the solution of constraints over the reals that contain both universal and existential quantifiers. For solving this problem we formulate it as a program in a…

In order to give appropriate semantics to qualitative conditionals of the form "if A then normally B", ordinal conditional functions (OCFs) ranking the possible worlds according to their degree of plausibility can be used. An OCF accepting…

Recent developments in termination analysis for declarative programs emphasize the use of appropriate models for the logical theory representing the program at stake as a generic approach to prove termination of declarative programs. In…

We study the question of whether a given regular language of finite trees can be defined in first-order logic. We develop an algebraic approach to address this question and we use it to derive several necessary and sufficient conditions for…

First-order logic has been established as an important tool for modeling and verifying intricate systems such as distributed protocols and concurrent systems. These systems are parametric in the number of nodes in the network or the number…

Lin and Zhaos theorem on loop formulas states that in the propositional case the stable model semantics of a logic program can be completely characterized by propositional loop formulas, but this result does not fully carry over to the…

We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient language to express non-termination. Of course, such property is…

We study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications are given as…

Semantics of logic programs has been given by proof theory, model theory and by fixpoint of the immediate-consequence operator. If clausal logic is a programming language, then it should also have a compositional semantics. Compositional…

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper,…

First-order logic is typically presented as the study of deduction in a setting with elementary quantification. In this paper, we take another vantage point and conceptualize first-order logic as a linear space that encodes "plausibility".…

We introduce a proper display calculus for first-order logic, of which we prove soundness, completeness, conservativity, subformula property and cut elimination via a Belnap-style metatheorem. All inference rules are closed under uniform…