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
votes
0answers
21 views

Translate the following sentence with the terms indicated into a quantified FOL sentence

All the leaves are brown, and the sky is grey. ($L$: ‘is a leaf’; $B$: ‘is brown’; $G$: ‘is grey’; $s$: an individual constant denoting the sky) I am unsure if I am correct, please provide some ...
1
vote
1answer
67 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 ...
0
votes
1answer
37 views

Relational Algebra: existential quantifiers

So i have the following question and template answer: Question: List the names of managers who have at least one dependant. Answer: {e.Fname, e.Lname | EMPLOYEE(e) AND (∃d)(∃t)(DEPARTMENT(d) AND ...
0
votes
1answer
20 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 ...
0
votes
0answers
20 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 ...
1
vote
0answers
11 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 ...
1
vote
0answers
30 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 ...
0
votes
0answers
41 views

A necessary condition for a relation to be in 2NF but not in 3NF is that some non-prime attribute must be determined by a non-prime attribute

I will state the complete question now, since it did not fit in the title. Is the statement given below correct? A necessary condition for a relation to be in 2NF but not in 3NF is that some non-...
1
vote
0answers
15 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 $...
4
votes
0answers
39 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,...
1
vote
0answers
35 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 ...
1
vote
0answers
15 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). ...
0
votes
1answer
37 views

Functional Abbreviation for Inst Expression in Turing's 1936 Paper

In Turing's 1936 paper On Computable Numbers Page 30-31, and its Correction Page 1-2 : For a Turing Machine $M$, $Inst(q_i S_j S_k L q_l ) $ means that if $M$ scans symbol $S_j $ under $m-...
0
votes
0answers
20 views

Is Inductive Logic Programming approach applicable to general theories (not just sets of Horn clauses)?

Inductive Logic Programming (https://en.wikipedia.org/wiki/Inductive_logic_programming) find hypothesis theory H for background theory B and set of examples E. ILP algorithms and implementations ...
2
votes
1answer
26 views

first order logic to normal form order of operations

∃y∀x [A(x) ∧ B(y) -> C(x,y)] ∃y∀x [¬(A(x) ∧ B(y)) v C(x,y)] ∃y∀x [¬A(x) v ¬B(y) v C(x,y)] I need to convert the above to conjunctive normal form. I'm a ...
0
votes
1answer
41 views

Does FOL extended with least-fixed points satisfy the Compactness Theorem?

I am aware that first-order logics (FOL) satisfies the compactness theorem. That is, if a FOL theory is insatisfiable, a finite subset of the axioms of such theory is insatisfiable too. Is it the case ...
3
votes
1answer
62 views

How to describe Deterministic Transitive Closure in FOL?

In "Finite Model Theory and Its Applications", page 152, it is said that Deterministic Transitive Closure, on ordered finite structures, captures LOGSPACE. Hence, taking into account that ...
1
vote
0answers
49 views

How to write “∀x.F(x)” for “F(x)=λx.Φ(x)” in one expression (sequel from question about “∀(λφ. (φ x m→ φ y))”?

This question is sequel from How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"? which further explains the notation and context. So - I have anonymous Boolean-valued ...
2
votes
1answer
311 views

How to understand quantifier without predication “ ∀(λφ. (φ x m→ φ y))”?

I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent ...
0
votes
1answer
47 views

Consistent theory based on L and not(A->A) is a theorem

I am working on this problem in which I have a theory $T$ based on language $\mathcal{L}$ and the only information we have is that T is consistent and $\vdash \lnot(A \rightarrow A)$. Given this ...
0
votes
0answers
28 views

Situation calculus: how to find pre-conditions in 15-puzzle game?

I have been working on finding the preconditions for a situation calculus example for some time now. This example is called the game "15-puzzle" where you can find a discription here https://...
2
votes
1answer
79 views

Expressing functions using the arithmetic dictionary

i have seen in the "logic to cs" class i take - a theorem that states: "every recursive (computable) function $f$ can be expressed using the arithmetic dictionary {$C_0, C_1, f_+(,), f_x(,), R_\le(,)$}...
0
votes
0answers
32 views

Show that exist a finite set of clauses F in first-order logic that Res*(F) is infinite

I'm kind of desperate at this point about this question. A predicate-logic resolution derivation of a clause $C$ from a set of clauses $F$ is a sequence of clauses $C_1,\dots,C_m$, with $C_m = C$ ...
2
votes
1answer
40 views

Unification Algorithm without Occur Check

I have been reading about Unification algorithm here https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm . And I wonder about the importance of occur check. I know ...
0
votes
1answer
46 views

Z-Specification = Routes

Im trying to make an invariant for this Z schema about routes. 1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
2
votes
1answer
111 views

Natural deduction: understanding bottom elimination (¬e)

I am new to natural deduction and upon reading about various methods online, I came across the rule of bottom-elimination in the following example. I do not understand the step in line 10. Upon ...
0
votes
0answers
42 views

Abstract syntax tree: expression->operation->lhs|rhs vs expression->lhs|operation|rhs - what should I take into account in decision?

I am trying to build class hierarchy for the abstract syntax tree of First Order Logic as specified in the grammar https://github.com/antlr/grammars-v4/blob/master/fol/fol.g4 (ANTLR parser generator). ...
2
votes
1answer
32 views

Why is the satisfiability of ESO formulas not equal to the satisfiability of FO formulas?

Existential second-order logic (ESO) formulas have the form $$\Phi = \exists R_1 ... \exists R_k. \phi$$ where $R_1...R_k$ are relation symbols and $\phi$ is a FO formula, which can use the relation ...
2
votes
1answer
92 views

Natural deduction proof: distributivity of existential quantification

In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic: $(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,...
2
votes
0answers
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 ...
1
vote
1answer
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 ...
1
vote
0answers
121 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 ...
2
votes
0answers
29 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 ...
1
vote
1answer
54 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 ...
0
votes
0answers
30 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"...
3
votes
1answer
94 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 ...
2
votes
1answer
49 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 ...
-2
votes
2answers
83 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 ...
0
votes
0answers
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-...
0
votes
1answer
34 views

What can't guarded fragment of FO express?

I have some basic confusions about the definition of the guarded fragment of first-order logic. Hopefully someone can tell me where I'm wrong. GF in FO is defined by: Atomic formulas, $x=y$ and $R(...
1
vote
3answers
166 views

Can undecidability theorems be detected by a machine? [closed]

this question was originally written in mathoverflow, but a comment recommended me to rewrite it as a CS question. This is not a mathematically formalized question. I'm sorry for that but think it's ...
1
vote
1answer
135 views

Algorithm for automatic construction of natural deduction proofs

I was wondering if there exists any algorithm for automatic construction of nautral deduction proofs. I'm interested in propositional logic and first order logic. If there is no algoritm, can you ...
1
vote
1answer
32 views

Logical characterization of $NC^1$

Morioka in his 2005 dissertation [1] referenced "On Uniformity within $NC^1$" by Barrington, Immerman, and Straubing. Using the following statement: Every $\mathbf{NC^1}$-predicate is computed by ...
1
vote
0answers
64 views

How can I compute the most general unifier for these two expressions?

I have the following first order logic expressions: $f(g(a, h(b)), g(x, y)),~f(g(z,y), g(y, y))$ and I want to compute the most general unifier for them. If I follow the algorithm found on these ...
1
vote
1answer
79 views

MSO (Monadic second-order logic) Logic On Words

Let L be a language over $\Sigma = \{a,b,c\}$ that contains all words, where the length $|w|_b$ (number of all b's) has remainder 1 if divided by 3. MSO logic over words are definded as follow: I ...
0
votes
2answers
765 views

The barbers paradox first order logic formalization

I tried to look on the site and while I found some similar questions, I did not find the first order logic formalization of the following sentence (the basic barber's paradox), so I wanted to ask if I ...
3
votes
1answer
63 views

Basic second-order logic example contains a mistake?

I'm reading the following course on second-order logic, by Péter Mekis : http://phil.elte.hu/mekis/sol.pdf . The course seems excellent, but I'm stuck on one of his first examples for showing the ...
1
vote
1answer
32 views

List of all possible reasoning tasks - satisfiability and theorem proving only?

What is the exhaustive list of reasoning tasks? As far as I can understand, then any logical reasoning reduces to 2 tasks only: 1) satisfiability problem (finding the assignment of the variables) and ...
5
votes
2answers
2k views

Why do ¬, ∀ and ∃ have the same precedence?

I thought the order of precedence of operators and quantifiers was arbitrary, but I don't really understand why those three have the same "strength" in relation to other operators (e.g., ¬ will have ...
2
votes
0answers
54 views

Ontology Editor or Something Else (in my case)? [closed]

Does there exist a system, e.g., software, an environment, a programming language, or the like, to represent knowledge and to reason with it, to query with, where the (descriptive) language used is at ...