The tag has no wiki summary.

learn more… | top users | synonyms

2
votes
1answer
78 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
35 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
36 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
35 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
15 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 ...
2
votes
1answer
76 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
25 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
35 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
55 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
208 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
56 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 ...
0
votes
0answers
23 views

Are these CNF clauses for at most one and the same correct?

Given Boolean variable Xij that represents whether dog i is kept in kennel j. Encode in CNF clauses: Dogs that cannot be kept together must be kept in separate kennels Here is what I ...
3
votes
2answers
59 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
103 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
194 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
38 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
158 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
70 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
118 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
123 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 $\{<, ...
5
votes
1answer
161 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
103 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
115 views

Decidability over finite graphs of small degree

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
216 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
149 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 ...
2
votes
1answer
121 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
517 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
158 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 ...
2
votes
1answer
200 views

Negation of nested quantifiers

The problem is: $$\exists x \forall y (x \ge y)$$ With a domain of all real positive integers. The negation is: $$\forall x \exists y (x < y)$$ so, if $y = x + 1$, the negation is true. That ...