# 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
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 ...
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, ...
394 views

59 views

47 views

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

Does every 3CNF propositional formula has an equisatisfiable 2CNF propositional formula?
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 ...
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 ...
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 ...
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 ...
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. ...
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 ...
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 ...
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 ...
131 views

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 ...
329 views

I'm trying to solve an exercise on inductive definitions, the premiss is: Let $\to$ be a relation on $A$ and $\to^*$ its reflexive, transitive closure, which is defined by following two rules: $a \... 0answers 143 views ### Understanding quantifiers I'm reading a paper by David Monniaux An encoding of array verification problems into array-free Horn clauses. Second page Line 10: "Very often, desirable properties over arrays are universally ... 1answer 73 views ### Encoding first order formula (or its tree) into binary string? How to encode a first order formula into binary string, which I could give as input to Turing machine or program to do something with it (deciding is it satisfiable, or is concrete structure model for ... 1answer 52 views ### Formally proving properties of fold function Recall the fold function for lists:$fold(f,z,[x,xs]) = fold(f,f(z,x),xs)fold(f,z,[]) = z$I want to formally proof that if$f$is associative, commutative and idempotent (meaning$f(x,y) = f(x,...
144 views

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 ...
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 ...
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 ...
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 ~ \...
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 ...
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), ...
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 ...
334 views

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 ...