# Questions tagged [first-order-logic]

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

153 questions
Filter by
Sorted by
Tagged with
1answer
264 views

### First Order Logic, First Order Logic + Recurrence and SQL

we know that SQL standard is equivalent to First Order Logic (FOL). I've seen at my lecture that graph connectivity cannot be expressed by FOL, so in SQL as well. But we know that we can easily solve ...
2answers
79 views

### Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?

Recently I was reading again this propositions as types paper by Philip Wadler: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf It gives an impression, ...
2answers
394 views

2answers
59 views

1answer
47 views

### Does every 3CNF propositional formula has an equisatisfiable 2CNF propositional formula

Does every 3CNF propositional formula has an equisatisfiable 2CNF propositional formula?
1answer
116 views

### Does every 3CNF propositional formula has an equivalent 2CNF propositional formula?

Does every 3CNF propositional formula has an equivalent 2CNF propositional formula? Definitions: 3CNF propositional formula is conjunctive normal form propositional formula, which is just ...
1answer
64 views

### Why do TPTP Performance plots look like this?

CASC is the premier Automated Theorem Prover competition performed annually at the Conference on Automated Deduction (CADE). The 2017 event has finished on the 9th of August this year. During this ...
0answers
89 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 ...
1answer
299 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 ...
1answer
34 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. ...
1answer
82 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 ...
1answer
108 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 ...
1answer
70 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 ...
0answers
131 views

0answers
110 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 ...
2answers
329 views

1answer
144 views

### Exercise about First-order logic

I try to express the following statements in first order logic: X is a subset of Y. A set can be uniquely characterised by its elements. The power set p(X) contains all subsets of X. A set X is the ...
1answer
22 views

### Constructing logical sentences that involve negative integers over the nonnegative integers

Consider the following statement: If $x$ and $y$ are integers and $z$ is a nonnegative integer and $x + z = y$, then $x$ is at most $y$. I'd like to build a sentence for this statement in the ...
1answer
54 views

### In the Resolution equivalence ($\neg A \implies B, B \implies C \models \neg A \implies C$) must $A$ be negated?

The sheet of equivalences given to us in class provides the the equivalences \begin{array}{|c|c|c|} \hline \text{Resolution} & A \vee B, \neg B \vee C \models A \vee C & \neg A \implies B, B ...
0answers
33 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 ~ \...
1answer
88 views

### Formal specification; Logical formula

* Initial Question * I'm trying to write a logical formula consists of three Boolean variable C1, C2, C3. My program takes graph as input and checks properties about them. C1 represents presence of ...
1answer
129 views

### Ehrenfeucht-Fraïssé games, possible mistake in example

I was reading up on Ehrenfeucht-Fraïssé and came by this example at http://www.math.cornell.edu/~mec/Summer2009/Raluca/lesson3.html Shouldn't there be a line between b4 and b2 (or b3 and b1), ...
0answers
78 views

### In ontology development, where do axioms come from?

I am developing an ontology. I've got the classes, relationships and I guess I could come up with instances at this point too. But what I'm really focused on is the axioms. I've learnt that the ...
2answers
334 views

7answers
8k 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 ...
1answer
1k 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 ...
1answer
231 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?