Questions tagged [first-order-logic]
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.
12
questions
2
votes
1answer
178 views
What is the set of all minimal 3CNF formulas?
Definition: A minimal 3CNF formula is an unsatisfiable 3CNF formula with minimum clauses connected by conjunctions, where each clause is disjunction of 3 literals, that is if any of it's clauses is ...
2
votes
1answer
2k 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 ...
20
votes
4answers
6k views
Can proof by contradiction work without the law of excluded middle?
I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my ...
7
votes
3answers
4k 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 ...
7
votes
1answer
746 views
Algorithm for deciding alpha-equivalence of terms in languages with bindings
I am interested in the alpha equivalence relation in languages with variable bindings, such as:
...
2
votes
1answer
308 views
How to understand quantifier without predication “ ∀(λφ. (φ x m→ φ y))”?
I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent ...
1
vote
1answer
43 views
What is the largest possible minimal 3CNF formula as function of the number of variables?
I have already defined here what is minimal 3CNF formula.
In the answer to the question, D.W. answered:
What you are thinking is wrong. A minimal, unsatisfiable formula can have more than 8 clauses.
...
1
vote
1answer
574 views
Convert conjunctive normal form to equivalent boolean formula with only NAND 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 NAND gates with ...
2
votes
1answer
4k 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 ...
1
vote
1answer
70 views
MSO (Monadic second-order logic) Logic On Words
Let L be a language over $\Sigma = \{a,b,c\}$ that contains all words, where the length $|w|_b$ (number of all b's) has remainder 1 if divided by 3.
MSO logic over words are definded as follow:
I ...
1
vote
0answers
115 views
Proving a first order logic theorem in equational logic with a term rewriting system
I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean ...
1
vote
0answers
35 views
What does the structure ($S_t^x P$) in this Existantial Instantiation imply, Skolemization?
The sheet of equivalences given to us in class provides the two equivalences
\begin{array}{|c|c|c|}
\hline
\text{Universal Instantiation} & \forall x ~ P(x) \implies {S_t}^x P & \exists y ~ \...
