# Questions tagged [first-order-logic]

First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.

182 questions
Filter by
Sorted by
Tagged with
33 views

### Help me understand whether these critical pairs are joinable

I have the following TRS $R$: $$l_1 = f(g(x)) \to f(x) = r_1 \\ l_2 = g(f(y)) \to g(y) = r_2$$ I want to know if $R$ is confluent, and whether $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$. I have ...
12 views

### What is the space-complexity of a boolean first-order query?

I have the intuitition that, if we implement a (space-efficient) boolean first-order query solver, the amount of consumed memory should depend on the data size (i.e., it should not be constant). ...
33 views

65 views

### Sample applications based on First Order Logic

I often hear about benefits of FOL, but I wonder what are some of its real world applications? Could someone please provide samples/case studies of applications of FOL that address real world ...
28 views

### In first order logic, how do we normally represent a statement?

I wanted for an example such as: Everyone has a mother. I've seen that it is represented in FOL as: $\forall x \exists y:$ Mother(x, y) I'm seeing that as:For every x, there exists a y, such that y ...
105 views

### Proving a first order logic theorem in equational logic with a term rewriting system

I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean ...
13 views

### Synthesis of the crisp programs from the Bayesian (probabilistic) programs?

https://arxiv.org/abs/2001.00805 is the article which is pointing towards the direction that the optimal policy of the reinforcement learning can be expressed as the Bayesian/probabilistic program (...
29 views

### Bounds on the size of the universe of a model for an FO-sentence

Sorry for the weird title. The Problem: Consider the first-order logic sentence φ≡∃s∃t∃u∀v∀w∀x∀yψ(s,t,u,v,w,x,y) where ψ(s,t,u,v,w,x,y,) is a quantifier-free first-order logic formula using ...
20 views

### Can full first order knowledge base be written as the single sequent in the sequent calculus?

The knowledge base of the first order logic essentially is single formula: conjunction of individual formulas (I guess, I am right). The sequent for the sequent calculus is the formula in the special ...
16 views

### Is it possible to write down every Prolog program+query as the sequent in the sequent calculus?

Prolog program P is set of Horn (definite) clauses, effectively it is the conjunction of implicational formulas. I guess that every Prolog program P with some query Q can be written as ...
28 views

### How to prove following two statements are equivalent in Hilbert System?

statement 1: $Γ$ is satisfiable implies $Γ$ is consistent. statement 2: If $Γ$ derives $α$ then $Γ$ entails $α$. I can easily prove statement 1 from 2 , but not 2 from 1 (without using strong ...
49 views

### General resolution in first order logic

Assuming you have a formula in first order logic like $$(\forall_x p(x) \land \forall_x q(x)) \rightarrow \forall_x(p(x) \land q(x))$$ (which seems valid?) Converting the formula to ...
29 views

### Is FOL representation of probabilistic assignment statement correct?

For instance, $x = x + 1[0.3]x+2$ sets $x$ to $x + 1$ with probability $0.3$ and to $x+2$ with probability $0.7$. If I use notation used in the paper "An Analysis of First-Order Logics of Probability"...
65 views

### Combining Predicate Logic and BigO

I am a beginner to predicate logic and BigO and am having though time understanding the definition of BigO in terms of predicate logic in the picture attached. I particularly am unable to understand ...
43 views

### On satisfiability for 2-variable FOL being NEXPTIME-complete

Let $\mathbf{FO^2}$ be the fragment of first-order logic consisting of sentences with at most two variables and no function symbols. It is well known that satisfiability for $\mathbf{FO}^2$ is ...
51 views

### How to correctly negate a predicate bounded by some quantifiers?

this is a problem which was asked in GATE CS 2010. This is question statement: Q: Suppose the predicate F(x, y, t) is used to represent the statement that person x can fool person y at time t. which ...
35 views

### How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?

I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-...