# Questions tagged [first-order-logic]

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

181 questions
Filter by
Sorted by
Tagged with
561 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 ...
115 views

### Convert conjunctive normal form to equivalent boolean formula with only NOR 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 NOR gates with ...
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. ...
123 views

### What is the set of all maximal 3CNF formulas?

Definition: A maximal 3CNF formula is satisfiable 3CNF formula, but if you conjuct it with another any new different 3 disjuctive literals clause, then the formula becomes unsatisfiable. Please don't ...
176 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 ...
73 views

### Implementing abduction over first order theories

I am interested in implementing abduction over a full first order theory ie it may be non-Horn. (Aside: Almost all the references I've seen for abduction operate over Horn theories eg "Modeling ...
134 views

458 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 ...
153 views

### Computing critical pairs, confluence and Normal terms

Down below is a Term rewriting system where I am trying to find the critical pairs, decide if it is confluent and find the Normal terms. I think it's difficult to understand all these concepts and I ...
469 views

777 views

### how can i know if a First order logic sentences is valid or unsatisfiable or neither?

i have trouble with understand this type of questions , i know how i can determine if the sentences is valid or unsatisfiable in Propositional logic , but in FOL i can't for example , i have the ...
68 views

### Resolution in First Order Logic

i have problem with resolution in first order logic i have : C1 : Ā¬ Loves(x,F(x) ) or Loves ( G(x) , x ) and ...
48 views

### Precedence of satisfiability operator

I'm just reading a textbook in mathematical logic, as following: What is the precedence to consider the equality and satisfiability operators in the equation pinpointed in red?! In other words, which ...
529 views

### in refutation (resolution) can we use a clause that have been resolved

In resolution if we have a set S composed of three clause C1, C2 and C3 and we want to proof that C4 is derivable from S using refutation: suppose we've resolved C1 and C2 to C5, can we resolve C1 ...
540 views

### How would one prove the pigeonhole principle with a SAT solver?

Suppose I wanted to find a proof of the pigeonhole principle or show that no proof shorter than $L$ exists. I understand that proof-checking is in NP, so I could write a CNF formula that is ...
12k views

### Why is A implies B true if A is false and B is false?

It seems to me that the 'implies' in English language does not mean the same thing as the logical operator 'implies', in a similar way how 'OR' word in most cases means 'Exclusive OR' in our everyday ...
2k views

### How can unifying 2 sentences in first-order logic result in a variable becoming 2 different things?

I'm working on a program which must use inference in first-order logic, and everything is working great except for 1 thing which I don't understand. The book I'm using, "Artificial Intelligence A ...
292 views

### Expressing 3-SAT in first-order logic

i read that First-Order Logic is strong enough to formalise all of Set Theory and thereby virtually all of Mathematics. How would you express in First-Order Logic the theorem: 3SAT is NP-complete?
294 views

### Using existential quantifier within implication

I had used an existential quantifier within an implication, as below: $$\exists ~ \sigma_{opt}~~~ \wedge~~~ n \in R^{+}~ ,~0<n<1 \rightarrow ~~ \sigma_{opt} = n$$ I've, recently, found that ...
71 views

### Is this formula valid?

is this formula valid ??, if it is not what interpretation could i use ? (ā x: P(x) -> ā x: Q(x)) -> ā x: (P(x) -> Q(x)). PS : i know that the other implication is valid.
704 views

### Quantified Boolean Formula vs First-order logic

Is Quantified Boolean Formula (QBF) the same as First-order logic (FOL)?
831 views

### Why is first-order logic (without arithmetic) VALIDITY only recursively enumerable, and not recursive?

Papadimitriou's "Computational Complexity" states that VALIDITY, the problem of deciding whether a first-order logic (without arithmetic) formula is valid, is recursively enumerable. This follows from ...
3k views

### Predicate Logic Notation: What does a “dot” mean?

What does a dot (.) mean in predicates? $\forall a \in A. \exists d \in D. H(a,d)$ Especially, how is the above different to $\exists d \in D. \forall a \in A. H(a,d)$ I've never seen this used ...