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

learn more… | top users | synonyms

7
votes
3answers
512 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
votes
0answers
24 views

How to write Boolean search expression?

I was reading the Kenneth Rosen's Discrete Mathematics books and trying to solve the exercise of the same. Where i came along with these question likes, What Boolean search would you use to look ...
1
vote
2answers
53 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
43 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
44 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
69 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
58 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
63 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
37 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
42 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
34 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
128 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
151 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
48 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
122 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
120 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
651 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
117 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
145 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
95 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
95 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
22 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
118 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
38 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
67 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
270 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
186 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
76 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
242 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
110 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
140 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
276 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
115 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
432 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
399 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
216 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 ...
4
votes
2answers
203 views

First-order logic arity defines decidability?

I've read first-order logic is in general undecidable, and that could be decidable only when working with unary operators. (I think that's propositional logic, correct me if I am wrong) The question ...