Questions tagged [first-order-logic]

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

181 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
1answer
24 views

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 ...
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 ...
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 ...
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 ...
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 ...
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://...
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$ ...
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 ...
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). ...
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 (...
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 ...
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 ...
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 ...
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"...
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) ...
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-...
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? ...
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 ...
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 ...
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 ...
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 ...
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) ...
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.