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
0
votes
1answer
217 views

About the first order logic (valid, Unsatisfiable, Syntactically wrong)

I am in trouble , I searched a lot about how to solve this kind of questions but I did not get any answers. I understand how can I know when the sentences is valid and Unsatisfiable in propositional ...
0
votes
3answers
61 views

A graph in descriptive complexity - is $x$ already a vertex?

So suppose that there is an undirected graph with edge connections known. Now in first-order logic there is quantifier $\forall x$. Then does this automatically refer to vertexes, or can we use ...
0
votes
1answer
24 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
1answer
148 views

Is it possible to encode logical expression and interpret it with SQL?

Is it possible without any forms of eval or stored procedures to execute a query, which interprets logical expression, encoded in some way in a table (or two tables)...
0
votes
1answer
250 views

Real world applications of first order logic

I study an AI course and we done some lectures about first order logic and the first thing that I was thinking is, what are the real world applications of first order logic and generally logical ...
0
votes
1answer
398 views

First Order Logic, First Order Logic + Recurrence and SQL

we know that SQL standard is equivalent to First Order Logic (FOL). I've seen at my lecture that graph connectivity cannot be expressed by FOL, so in SQL as well. But we know that we can easily solve ...
0
votes
1answer
35 views

Finding Models for a sequent

I am trying to generate models for the following sequent. $$\exists x \exists y \forall z (z = x \lor z = y)$$ What I have come up with is this. $$A= \{0,1\}$$ So in this model, for all the values ...
0
votes
2answers
433 views

When is a first-order formula is existential and when is it universal?

So I have a few questions about determining which formula it is: So if a binary predicate symbol $X$ denotes an edge between two variables, say $x$ and $y$, for the following formulas Why is $\...
0
votes
1answer
76 views

a program discovering himself how to solve propositional calculus

it is well-known that propositional logic problems such as $$ (p\leftrightarrow q) \lor r \quad\overset{?}{\vdash}\quad (((p\lor q)\to(p\land q)) \land \lnot r)\lor r$$ can be simply solved by ...
0
votes
1answer
371 views

Relations between statements involving universal quantifier, conditional and biconditional

If we consider two predicates: $b(x)$: x is a boy $c(x)$: x is clever Then, there are four statements involving $∀, b(x), c(x), →$ and $↔$ . These are below along with my interpretation of their ...
0
votes
0answers
16 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 ...
0
votes
1answer
26 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 ...
0
votes
1answer
40 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://...
0
votes
0answers
26 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$ ...
0
votes
1answer
33 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 ...
0
votes
0answers
27 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). ...
0
votes
0answers
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 (...
0
votes
0answers
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 ...
0
votes
0answers
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 ...
0
votes
0answers
15 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 ...
0
votes
0answers
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"...
0
votes
0answers
16 views

How to compute (partial) consequence set for premises of the first order logic?

I am playing with the Sequent Calculus Trainer https://www.uni-kassel.de/eecs/fachgebiete/fmv/projects/sequent-calculus-trainer.html . It is game with judgments, where each judgment consists from: 1) ...
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
0answers
48 views

Description logic representation

If Manufacturer manufactures electronic equipment, then manufacturer generates e-waste. I have generated the triple. However how to represent the if-then statement in DL? ...
0
votes
0answers
28 views

Show the Invalidity of the sequence

∃x (P(x) → Q(x)), ∃x P(x) ⊨ ∃x Q(x) I am trying to find the invalidity of the following sequents. A = Set of natural number P(x) : x is odd Q(x) : x is not divisible by 2 What i don't understand ...
0
votes
0answers
113 views

Convert conjunctive normal form to equivalent boolean formula with only NOR gates

Let $\varphi$ be a boolean formula in 3-CNF form (conjunctive normal form with three literals at most per clause). I want to convert it to an equivalent boolean formula that uses only NOR gates with ...
0
votes
0answers
46 views

Precedence of satisfiability operator

I'm just reading a textbook in mathematical logic, as following: What is the precedence to consider the equality and satisfiability operators in the equation pinpointed in red?! In other words, which ...
0
votes
0answers
88 views

What does an = sign with an x beneath it mean?

I am studying for a test in Logic right now, and saw the symbol $\underset{x}{=}$, which is used like this: $I \underset{x}{=} I'$. I've seen it in the solutions of questions like this one: Prove ...
-1
votes
1answer
67 views

predicate logic/binary relation help

(1) ∀x, y, z (x < y ∧ y < z → x < z) (transitivity) (2) ∀x ¬(x < x) (antisymmetry) (3) ∀x, y (x < y ∨ x = y ∨ y < x) (linearity) I need to give an example of a (nonempty) ...
-3
votes
1answer
69 views

Is this formula valid?

is this formula valid ??, if it is not what interpretation could i use ? (∀ x: P(x) -> ∀ x: Q(x)) -> ∀ x: (P(x) -> Q(x)). PS : i know that the other implication is valid.

1 2 3
4