Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [first-order-logic]

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

Filter by
Sorted by
Tagged with
1 vote
1 answer
129 views

Resolution on weakening rule by derived clause

How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule: $\frac{C} {C \vee D}$ (A clause $C$ is implied by $F$ if for ...
A. H.'s user avatar
  • 498
4 votes
0 answers
71 views

Extending Fagin's Theorem to the Polynomial Hierarchy

Fagin's Theorem (see Wikipedia and these lecture notes) states that there is an equivalence between second-order logic (SOL) formulas with existential quantifiers, and problems in NP. I was wondering ...
UserA2000's user avatar
0 votes
0 answers
6 views

Datalog+- doubt about semantics and complexity

I am reading about Datalog+- (e,g, https://ieeexplore.ieee.org/abstract/document/5571709), and I have a doubt about its semantics, and about the complexity of query answering. In Datalog+-, you write ...
441Juggler's user avatar
1 vote
0 answers
37 views

How do I prove relations of two CTL formulas?

If I have two CTL equations, how do I prove they're equivalent or that one implies the other? What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
JobHunter69's user avatar
3 votes
1 answer
171 views

how to do incremental construction of the minimal model in logic programming?

I was reading a book titled "Essentials of Logic Programming.", most parts of the book are easy to understand. but now having a problem with Theme 45: incremental constructions of the ...
alim's user avatar
  • 1,014
0 votes
1 answer
128 views

Is any 2-CNF has 2-DNF representation?

I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
FirePapaya's user avatar
0 votes
2 answers
156 views

Can you help me in finding an algorithm that finds the first unique number in an array with lowest position?

I have the following problem to solve: Given a non-empty array A consisting of N integers, the task is to find the first unique number in the array. A unique number is defined as a number that occurs ...
Ardita Morina's user avatar
2 votes
2 answers
91 views

'Someone' in first order logic

I have in the lectures a sentence in English, which I have to translate to First Order Logic. Someone who loves all animals loves all humans. Textbook solution: ∀x.(is_human(x) ⇒ is_animal (x)) ⇒ ∀...
Gunners 's user avatar
0 votes
0 answers
47 views

Minimum DNF length of a conjuction of equivalences

Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses. I am puzzled on what approach to take -- whether to ...
DesmondMiles's user avatar
1 vote
0 answers
90 views

Understanding unprovable halting, model theory, and (in)completeness

I know computability, but not model theory and logic, so this question may be naive or confused in that respect. A blog post of Scott Aaronson mentions a Turing Machine $M^*$ such that the statement P:...
usul's user avatar
  • 4,129
0 votes
1 answer
54 views

How substituituion composition is associative?

I'm not convinced that substitutions are associative, I read the https://en.wikipedia.org/wiki/Substitution_(logic)#First-order_logic and the https://www.youtube.com/watch?v=_cVNeccMF-E My problem is ...
geckos's user avatar
  • 243
1 vote
1 answer
55 views

Substitutions unions vs composition are not the same?

I'm studying substitutions. A substitution is a set of mappings from variables to terms $\{a \rightarrow b; c \rightarrow d;...\}$. Given these substitutions: $\sigma_1 := \{x \rightarrow y\}$ $\...
geckos's user avatar
  • 243
1 vote
1 answer
78 views

Simple Skolemization Question

Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
Abhishek Manikandan's user avatar
0 votes
0 answers
52 views

First-Order logic exercise

I'm trying to solve the following exercise: Given this is true: \begin{align} \neg \forall x \space \ \exists y \ ( x\neq y \rightarrow LeftOf(x,y) )\end{align} Demonstrate : \begin{align} \exists y \...
eojpyd's user avatar
  • 1
0 votes
1 answer
671 views

Finding the loop invariant for Array Reversal

I've been assigned to find the loop invariant for the following code: ...
ifiht's user avatar
  • 103
1 vote
1 answer
43 views

What does :: indicate in all-quantifier predicates?

Can somebody explain to me the meaning of $::$ in the following predicate? $$(\forall i : P(i) : Q(i)) \equiv (\forall i :: P(i) \implies Q(i))$$
Rubus's user avatar
  • 123
1 vote
2 answers
198 views

Logical consequence problem, doubt

It is possible to have this logical consequence? $$ \forall x (p(x) \vee q(x)) \models \forall x p(x) \vee \forall x q(x) $$
caio a's user avatar
  • 13
1 vote
1 answer
60 views

Why we can't use deduction theorem on soundness to contravene second incompleteness with lob's theorem

I'm starting to learn modal logic and there is something that's bothering my mind for a while. we know from deduction theorem that $((\vdash q) \rightarrow (\vdash p)) \Leftrightarrow(\vdash (q \...
asha soroushpoor's user avatar
2 votes
1 answer
40 views

First-order model checking is not fixed parameter tractable on general graphs

I read that the problem of first-order model checking is believed to be not fixed parameter tractable on general graphs. Why is this the case? Would be happy about some reference Thanks in advance!
amhineoni's user avatar
1 vote
0 answers
24 views

Prove that any first-order logics with equality and a relation/functional symbol of arity more than 1 is undecidable

Definition: A formal logic system is decidable – if there is an algorithm that can determine if any given sentence is a theorem (or not). Based on this definition, I am not sure how to move to prove ...
Avv's user avatar
  • 505
-1 votes
2 answers
87 views

Is there a quantifier more powerful than the other to determine FOL connector?

So basically we have 2 types of quantifier in first order logic, they are universal quantifier and existential quantifier. Usually we use implies connector(->) when we have universal quantifier in ...
Thomas Iskandar's user avatar
0 votes
0 answers
30 views

How can I prove KB╞ α?

Is correct to use ~α as rule to prove KB╞ α? Is possible to unify sentence ~V(x,y) v S(x) with V(N,W)? ...
a.sarto's user avatar
1 vote
1 answer
34 views

First-order iteration operator example

I am reading on https://en.wikipedia.org/wiki/FO_(complexity)#Iterating that FO[$t(n)$] consists in first-order logic with an iteration operator that iterates $t(n)$ number of times some quantifier ...
441Juggler's user avatar
-1 votes
1 answer
72 views

Conjuctive Normal Form

Let f(P,Q,R) be the truth-function defined as follows. f(P,Q,R)=1 if and only if Q and R have different truth-values; or P and R have the same truth-values. Choose all formulas that are in conjunctive ...
Asghar Esfahani's user avatar
2 votes
1 answer
125 views

Resolution algorithm does not seem to generate the empty clause

Let's assume I have the following 3 clauses: $\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$ and I want to see if our KB entails $\neg U$ so I tried to apply ...
user127875's user avatar
0 votes
0 answers
40 views

Why is “For all the simple things you have done to me, there exists one thing that makes me happy” FALSE? Use nested quantifiers to prove your point

I've done my due dilligence and tried to answer this question using every resource I could get. KhanAcademy, NesoAcademy, and Rosen's Discrete Mathematics book. I still can't wrap my head around it. ...
Tuan's user avatar
  • 1
4 votes
1 answer
86 views

Uses of of the one-variable fragment of first-order logic aka S5

I'm looking at decidable fragments of first-order logic. It seems that FO(1), i.e. the one-variable fragment of first-order logic is equivalent to the modal logic S5. However, I cannot find a ...
Nicola Gigante's user avatar
0 votes
0 answers
38 views

Specific quantifier elimination for real algebraic numbers

It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
Theo Deep's user avatar
  • 113
1 vote
1 answer
52 views

Restriction in description logic

$Human ⊓ ¬Female ⊓ (∃married.Doctor) ⊓ (∀hasChild.(Doctor ⊔ Professor))$ Here, $∃married.Doctor$ means if there exists an individual who is married to Bob belongs to $Doctor$ concept. But my ...
Mahmudul Haque's user avatar
0 votes
1 answer
67 views

Domain of discourse vs First-order theory

In the question (Validity of predicate logic formulas) I see the following way of expressing: "The predicate $P(x,y) \equiv \bigl[ y \cdot x = 1 \bigr]$, where the domain of discourse is $\...
Theo Deep's user avatar
  • 113
1 vote
0 answers
97 views

SMT validity solvers/ quantifier elimination in Ocaml

I am working on my own expression package in Ocaml and have to perform both validity queries and quantifier elimination. I have already implemented Cooper's procedure (for Presburger and Linear ...
Theo Deep's user avatar
  • 113
6 votes
4 answers
4k views

How is ‘x + ½ = 2 and x ∈ ℤ’ an open statement?

I was watching this video on statements. There is an example: $x + \frac12 = 2$ It's an open statement as the truth value could be T or ...
Mahmudul Haque's user avatar
0 votes
1 answer
92 views

Mechanically proving element non-membership

I'm facing a (possibly simple) problem while proving a theorem. I need to show that under several (true) assumptions, some element is not in a set. Such assumptions are all met and there is are ...
Chaos's user avatar
  • 543
3 votes
1 answer
109 views

PetersonNP, mechanical mutual exclusion proof

Good day everyone, I'm currently trying to carry out the PetersonNP (a.k.a. FilterLock) correctness proof (mutual exclusion). I've found several proof sketches on concurrency books but I'm interested ...
Chaos's user avatar
  • 543
1 vote
1 answer
100 views

Incomplete definition of function- first order logic

Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations. Let $\Sigma_2=\{c',g^2,R_1'^1,...,R_k'^1\}$ where $c'$ is constant, $g$ is ...
Ella's user avatar
  • 109
2 votes
2 answers
115 views

Problem with formalism in first order logic

This is a general question in first order logic. Assume I have alphabet $\Sigma$ that contains one-argument function (among other symbols). I want a new alphabet, $\Sigma'$, which is the same as the ...
Ella's user avatar
  • 109
3 votes
1 answer
86 views

equivalence of validity above different alphabet

Given the next alphabets: $\,\,\Sigma_1=\{R^2,P^1,=^2\}\,\,,\Sigma_2=\{c,f^1,=^2\}.$ Prove of Disprove: There's exists an algorithm, that given formula $A$ above $\Sigma_2$, builds formula $A'$ above ...
Ella's user avatar
  • 109
2 votes
1 answer
28 views

non-existence of sentence that captured specific property

For a sentence $\varphi$, we'll define $Spec(\varphi)$ to be the set of all $n\in\mathbb{N}$ for which there is a model $M$ with $|D^M|=n$, such that $M\models\varphi$. Let $\Sigma=\{P(\cdot),R(\cdot)...
Ella's user avatar
  • 109
1 vote
1 answer
76 views

First-order logic - Does there exist a sentence that is satisfiable by all infinite models and only by them?

Prove or Disprove: There is $\boldsymbol{no}$ alphabet $\Sigma$ and closed formula (no free variables) $\varphi$ above $\Sigma$, such that for any Model $M$ it holds that $M\models\varphi\iff\,|D^M|=\...
Ella's user avatar
  • 109
1 vote
1 answer
42 views

Validity of formulas in very specific alphabet

Let $\Sigma = \{c_1, c_2, R(\cdot,\cdot) \}$ be an alphabet in first-order logic without $=$, where $c_1,$ $c_2$ are constant variables and $R$ is binary relation. Let $\varphi$ be a formula without ...
Ella's user avatar
  • 109
1 vote
1 answer
101 views

There is an $n^k$ prover if and only if $P = NP$

I am studying computational complexity using Papadimitrious's book: "Computational Complexity". I am trying to solve the final statement of Problem 8.4.9, but I am stuck and would like some ...
Gabriel F. Silva's user avatar
0 votes
1 answer
91 views

Tuple relational calculus: existential quantifiers

I have the following question and given answer: Question: List the names of managers who have at least one dependant. Answer: ...
pk00's user avatar
  • 27
0 votes
1 answer
24 views

Partitions of star-free languages and questions on the proof of the Splitting Lemma by Diekert/Gastin

I'm currently reading a paper on First-order definable languages by Volker Diekert and Paul Gastin. Im having trouble understanding a part of the proof for lemma 3.2 (splitting lemma). The part I'm ...
Algebruh's user avatar
  • 321
0 votes
0 answers
45 views

Practical ml model explainability with graphs and prolog

How practical are logic engines for proof paths combined with knowledge graphs in Providing reasonable explainability for ML models trained using GNNs? Adding more context. there is a history of ...
Sal Jr's user avatar
  • 141
1 vote
0 answers
20 views

Good exposition of tableau for first-order logic with equality?

I'm looking for a resource (online or printed) that explains in a self-contained way the classic tableau for first-order logic with equality. All I can find are expositions of tableaux for first-order ...
Nicola Gigante's user avatar
1 vote
0 answers
45 views

Multiple parameter predicates and the Relational Model

I've got a very general question about the relational model and it's relationship to 1st order predicate calculus. It will probably seem very basic to most, I'm afraid, a consequence of me grappling ...
Celine Atwood's user avatar
1 vote
0 answers
24 views

Modal logic equivalent to two-variable first-order logic?

It is well-known that many modal logics can be viewed as fragments of $FO^2$, i.e. two-variable first-order logic. But is there a modal logic that is not a fragment, but is expressively equivalent to $...
Nicola Gigante's user avatar
4 votes
0 answers
57 views

Do FOL theorem provers accept axiom schemata?

Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata? I looked in the Vampire "manual" briefly,...
MWB's user avatar
  • 505
1 vote
0 answers
46 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 ...
Dennis van den Berg's user avatar
1 vote
0 answers
55 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). ...
441Juggler's user avatar

1
2 3 4 5