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

learn more… | top users | synonyms

0
votes
0answers
25 views

How does the expressive power of CSS selectors compare to first-order logic?

Are there queries, that can be expressed in one, but cannot be in another?
0
votes
0answers
31 views

Deductive proof - need help, explanation how to [migrated]

I am working on assignment for school where the task asks to give a deductive proof. However, I have never used this technique (nor that I am very good in proofs in general) thus it is quite ...
7
votes
3answers
538 views

What is the relation between First Order Logic and First Order Theory?

I thought that any FOT is a subset of FOL, but that does not seem to be the case, because FOL is complete (every formula is either valid or invalid), while some FOT (like linear integer arithmetic) is ...
1
vote
2answers
62 views

Skolem constant in existential instantiation for first order logic

For any sentence $\alpha$, variable $v$, and constant symbol $k$ that does NOT appear elsewhere in KB: $$\dfrac{\exists \nu. \alpha}{\mathsf{subst}(\{ \nu / k \},\alpha)}.$$ E.g., $∃x. ...
3
votes
1answer
44 views

Equivalent formulae with different CNF

I was not able to find or come up with two formulae which are equivalent but have different CNF. All my ideas reduce to the same formula after applying transformations. The requirements are the ...
0
votes
1answer
45 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 ...
1
vote
1answer
71 views

Logic formula for exactly n unique objects (no more, no less)

I have a question in Logic: If I am asked to construct a formula, using the '=' predicate, that shows that there are exactly n objects, I need to show that there are no n+1 objects, right? For ...
0
votes
0answers
60 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
vote
0answers
10 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
0
votes
1answer
66 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
38 views

Statement true under minimal Herbrand model

Let's say I have a program like this: r(X, l(X)). r(X, t(Y,_)) :- r(X,Y). r(X, t(_,Z)) :- r(X,Z). Now the question is: is ¬r(a, l(b)) true in the minimum ...
2
votes
0answers
44 views

What is the difference between superposition and paramodulation?

I am currently writing a paper about automated theorem proving in first-order logic. Equality is not uncommon for mathematical problems and almost every theorem prover like VAMPIRE or SPASS has a ...
1
vote
0answers
32 views

Proving the following chain of implications

I'm struggling with a proof in the text for my logic course, and I'm wondering if someone could offer a hint or some help. The question is basically as follows. Show that if the decision problem for ...
0
votes
0answers
35 views

Is Prolog semi-decidible?

The first order logic is semi-decidible. If there is a correct sentence on the alphabet,which is a logical consequence, it is found. Instead if it isn't a logical consequence you can go in loop (or it ...
3
votes
1answer
138 views

Difference between First Order Logic and Predicate Calculus

I see the two used interchangeably. Is one the subset of the other or are they both the same thing?
2
votes
1answer
46 views

What can be concluded from a full application of resolution?

I know that resolution is refutation complete, but what can we conclude if a resolution procedure leads to a situation with no more chance to operate the resolution? Given a propositional formula ...
10
votes
1answer
157 views

Term rewriting; Compute critical pairs

I have tried to solve the following exercise but I got stuck while trying to find all the critical pairs. I have the following questions: How do I know which critical pair produced a new rule? How ...
1
vote
0answers
63 views

Undecidability of an existential theory

$F[u, u^{-1}]$ is a ring that contains the polynomials in $u$ and $u^{-1}$ with coefficients in the field $F$. Some theorems (from ...
3
votes
1answer
18 views

Extension of Tarski's result on the decidability of reals

Due to Tarski's result, it is well-known that the first-order theory of reals $(\mathbb{R},+,\cdot,<,=,0,1)$ is decidable. I am working on a paper where I need an extension of this result. More ...
1
vote
1answer
50 views

Can well-formed formulas in predicate logic for a given signature be recognized in LOGSPACE?

I read that visibly pushdown languages are supposed to model the typical simple formal languages like XML better than deterministic context free languages. The visibly pushdown languages can be ...
5
votes
4answers
123 views

Can I use ellipses in first order logic

I ask, because I have to come up with a first-order logic sentence that shows that there are exactly N objects in the universe. What I've been able to come up with is: $$ \forall x \; \exists y_1, ...
3
votes
2answers
123 views

Skolemization with multiple arguments — how to unify

Edit: answerers keep finding (valid!) problems with my example. I'll try again. The older version is below the horizontal line. Thanks to Klaus below for pointing out the last problem. My ...
3
votes
3answers
731 views

Can someone clarify this unification algorithm?

I've been having trouble understanding a unification algorithm for first order logic, as I don't know what a compound expression is. I googled it, but found nothing relevant. I also don't know what a ...
1
vote
1answer
122 views

Satisfiability of first-order logic is undecidable?

I struggle with understanding why the satisfiability in the first-order logic is undecidable. Could you explain it with some examples? I've also seen that satisfiability in some first-order formulas ...
2
votes
1answer
151 views

Propositional logic — syntactical completeness

Lets consider propositional logic. We say a proof system for propositional logic is syntactically (negation) complete if for every $\alpha$, either $\alpha$ or $\neg \alpha$ are provable within the ...
0
votes
3answers
52 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 ...
1
vote
1answer
98 views

How to prove that a predicate is prefix closed

Suppose we have the predicate $\qquad A.p.q ≡ (∀i \mid p≤i≤j<q : X.i≤X.j)$ which says that $X[p..q)$ is ascending. Apparently, the predicate holds for empty segments, is prefix closed and is ...
2
votes
1answer
96 views

Does Herbrand's theorem mean any first-order logic formula can be expressed in CNF?

Herbrand's theorem shows that any formula of first-order logic can be expressed as a disjunction of quantifier-free formulas of first-order logic. Is this equivalent to saying that Herbrand's theorem ...
2
votes
0answers
23 views

Completeness and first order logic with Least fixed point operator (LFP)

Is there any result about the extension of first order logic with least fixed point operator, being complete (as logic in general on infinite structures too) or not? In other words does the Goedel ...
4
votes
1answer
120 views

Solving SAT using tableau calculus

I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the ...
1
vote
1answer
29 views

Denumerably many isomorphism types

Computability and Logic by Boolos and Burgess says that formula $\Gamma_d$ in example 12.12 ∀x∀y(∃u(u ≠ x ∧ u ≡ x) ∧ ∃v(v ≠ y ∧ v ≡ y)) → x ≡ y) supports ...
4
votes
1answer
39 views

Should we not reuse constants in tableaux proofs?

I am trying to understand the proof of the following using tableaux: $$ \exists x\forall y.r(x,y) \to \forall x \exists y . r(x,y) $$ This is how it works out: $$ (1) \space \exists x \forall y ...
2
votes
1answer
69 views

FOL substitution - is it possible to substitute two variables with each other? e.g. $\theta=\{x/y,y/x\}$?

Let $C = m(P,X,Y) \leftarrow m(Q,X,Z), m(R,Z,Y)$. Is it possible to do the following substitution? $D = C\theta$ where $\theta = \{Q/R,R/Q\}$ s.t. $D = m(P,X,Y) \leftarrow m(R,X,Z),m(Q,Z,Y)$
2
votes
3answers
271 views

What is the point of (Compactness theorem in the) Overspill principle?

The principle (called a Löwenheim–Skolem theorem by Huth and Ryan) states Let $\phi$ be a sentence of predicate logic such that for any natural number $n \geq 1$, there is a model of $\phi$ with ...
1
vote
2answers
201 views

Can we move quantifiers to the left in predicate logic?

Say I have part of a query in the form: ∃xa(...)∧∃xb(...)∧∃xc(...), where a, b, and c are attributes and the ellipses can be anything (I'm looking for a general rule). Is this equivalent to saying ...
3
votes
2answers
77 views

Constructively deciding whether a decidable predicate holds universally

I am trying to obtain the proof of the proposition: $(\forall x \in \mathbb{N}, P(x)) \vee (\neg \forall x, P(x))$ given that the property $P$ is decidable for every $x \in \mathbb{N}$, i.e. ...
0
votes
1answer
1k views

Horn clause to Prolog [closed]

At the needs of my HW at uni I need to transform some Horn clauses to Prolog but I cannot figure out how to do it. I found out some guides but they describe how to do it with only one fact. So can you ...
3
votes
1answer
243 views

Why ⊢ for affirmative predicates and ⊨ for ¬negations?

I read a book which says that in Predicate Calculus, syntactic theorem proving is identical (complete and sound) with semantic entailment and this is very useful because it is easier to prove positive ...
1
vote
1answer
112 views

Logic Question - Why is This an Implication?

I have a question about predicate logic. Suppose we have the following predicates: $\text{Study}(x,y)$: x studies y $\text{Comp}(x)$: x is a computing student I want to encode the following ...
2
votes
4answers
179 views

No number is equal to Zero, is this statement true or false?

While reading an article on logic, there is a sentence "No number is equal to zero" and we have to assign truth values to this sentence. I hope this is true and the article says it as false. Can ...
5
votes
0answers
111 views

On the Turing Completeness of First Order Logic

It is well known that in Descriptive Complexity Theory FO is equivalent to AC0. However, this accepts a couple of a theory and a string <T,s> iff the ...
8
votes
1answer
133 views

Verify correctness of quantifier elimination, using SAT

Let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be $n$-vectors of boolean variables. I have a boolean predicate $Q(x,y)$ on $x,y$. I give my friend Priscilla $Q(x,y)$. In response, she gives me ...
4
votes
1answer
141 views

Characterising $(aa)^*$ in first order logic

In my descriptive complexity class, we've been asked to find a formula that characterises the language $(aa)^*$ (over the alphabet $\{a\}$) with a first order formula over the language $\{<, ...
6
votes
1answer
282 views

Differences between basic, complex and terminological facts in a Knowledge Base using First-Order Logic

I've been reading the excellent book Knowledge Representation and Reasoning by Ronald Brachman and Hector Levesque. In the beginning of Section 3.2 "Vocabulary" of Chapter 3 "Expressing Knowledge" ...
3
votes
2answers
116 views

Why do the sequent calculus NOT left and NOT right rules work?

The rules I am considering are $\frac{\neg A, \ \Gamma \implies \Delta}{\Gamma \implies \Delta, \ A} (\neg L)$ and $\frac{\Gamma \implies \Delta, \ \neg A}{A, \ \Gamma \implies \Delta} (\neg R)$ I am ...
4
votes
0answers
124 views

Decidability over finite graphs of small degree [closed]

Suppose $\sigma$ is a vocabulary of First Order logic consisting of one binary relation $E$ and let $\phi$ be a $\sigma$ sentence (FO formula with no free variables). Is it decidable whether there is ...
2
votes
1answer
439 views

first order logic resolution unification

Assuming I have shown part of the knowledge base in the clausal format: [1] p1(banana). [2] not p1(X) or p2(Y). [3] p1(X) or not p3(F). ... and more rules. ...
1
vote
1answer
415 views

Difference between intended interpretation and extended interpretation in first-order logic

I am currently reading "Artificial Intelligence - A modern approach" and I really do not get the difference between intended interpretation and extended interpretation in first-order logic. Are ...
3
votes
1answer
222 views

MGU and Variable Standardization - CNF

I have been reading on converting first order logic sentences to conjunctive normal form, and then performing resolution. One of the steps of converting to CNF, is to Standardize variables: rename ...
5
votes
2answers
1k views

Is resolution complete or only refutation-complete?

Going through some knowledge representation tutorials on resolution at the moment, and I came across slide 05.KR, no77. There it is mentioned that "the procedure is also complete". I think this ...