The first-order-logic tag has no wiki summary.
3
votes
2answers
78 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
101 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
97 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
55 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
49 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 ...
1
vote
2answers
96 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 ...
3
votes
2answers
120 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
112 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 ...
