Questions tagged [first-order-logic]

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

Filter by
Sorted by
Tagged with
1
vote
1answer
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 ...
0
votes
0answers
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 ...
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. ...
2
votes
1answer
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 ...
2
votes
1answer
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 ...
3
votes
1answer
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 ...
5
votes
0answers
134 views

Characterization of alpha-equivalence in languages with bindings

Following up on this post denoting $(x \leftrightarrow y)$ the permutation of $x$ and $y$ and $P[x \leftrightarrow y]$ the term obtained from the term $P$ by permuting $x$ and $y$ (so for example if $...
7
votes
1answer
737 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: ...
3
votes
1answer
130 views

What is the difference between $x:A$ and $x \Xi A$?

Given a type hierarchy $(\tau,\sqsubseteq)$ and a signature $(VSym, FSym, PSym, \alpha)$, one says that the typing function $\alpha$ assigns to each variable symbol $x \in VSym$ a non-empty type $A \...
4
votes
1answer
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 ...
1
vote
0answers
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 ...
2
votes
2answers
469 views

Induction rules for reflexive, transitive closure

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 \...
1
vote
0answers
178 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 ...
3
votes
1answer
83 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 ...
3
votes
1answer
169 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 ...
0
votes
1answer
226 views

About the first order logic (valid, Unsatisfiable, Syntactically wrong)

I am in trouble , I searched a lot about how to solve this kind of questions but I did not get any answers. I understand how can I know when the sentences is valid and Unsatisfiable in propositional ...
1
vote
1answer
23 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 ...
2
votes
1answer
59 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 ...
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 ~ \...
1
vote
1answer
91 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 ...
1
vote
1answer
165 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), ...
3
votes
0answers
79 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 ...
0
votes
2answers
449 views

When is a first-order formula is existential and when is it universal?

So I have a few questions about determining which formula it is: So if a binary predicate symbol $X$ denotes an edge between two variables, say $x$ and $y$, for the following formulas Why is $\...
2
votes
1answer
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 ...
3
votes
1answer
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 ...
1
vote
0answers
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 ...
4
votes
1answer
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 ...
3
votes
1answer
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 ...
24
votes
7answers
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 ...
4
votes
1answer
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 ...
1
vote
1answer
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?
1
vote
1answer
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 ...
-3
votes
1answer
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.
1
vote
1answer
704 views

Quantified Boolean Formula vs First-order logic

Is Quantified Boolean Formula (QBF) the same as First-order logic (FOL)?
7
votes
2answers
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 ...
5
votes
2answers
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 ...
8
votes
3answers
2k views

What is the relation between First Order Logic and First Order Theory?

I thought that any FOT is a subset of FOL, but that does not seem to be the case, because FOL is complete (every formula is either valid or invalid), while some FOT (like linear integer arithmetic) is ...
1
vote
2answers
1k views

Skolem constant in existential instantiation for first order logic

For any sentence $\alpha$, variable $v$, and constant symbol $k$ that does NOT appear elsewhere in KB: $$\dfrac{\exists \nu. \alpha}{\mathsf{subst}(\{ \nu / k \},\alpha)}.$$ E.g., $∃x. \mathrm{Crown}(...
2
votes
1answer
239 views

Equivalent formulae with different CNF

I was not able to find or come up with two formulae which are equivalent but have different CNF. All my ideas reduce to the same formula after applying transformations. The requirements are the ...
0
votes
1answer
76 views

a program discovering himself how to solve propositional calculus

it is well-known that propositional logic problems such as $$ (p\leftrightarrow q) \lor r \quad\overset{?}{\vdash}\quad (((p\lor q)\to(p\land q)) \land \lnot r)\lor r$$ can be simply solved by ...
1
vote
1answer
134 views

Logic formula for exactly n unique objects (no more, no less)

I have a question in Logic: If I am asked to construct a formula, using the '=' predicate, that shows that there are exactly n objects, I need to show that there are no n+1 objects, right? For ...
0
votes
0answers
88 views

What does an = sign with an x beneath it mean?

I am studying for a test in Logic right now, and saw the symbol $\underset{x}{=}$, which is used like this: $I \underset{x}{=} I'$. I've seen it in the solutions of questions like this one: Prove ...
2
votes
0answers
29 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
0
votes
1answer
400 views

Relations between statements involving universal quantifier, conditional and biconditional

If we consider two predicates: $b(x)$: x is a boy $c(x)$: x is clever Then, there are four statements involving $∀, b(x), c(x), →$ and $↔$ . These are below along with my interpretation of their ...
1
vote
0answers
178 views

Proving the following chain of implications

I'm struggling with a proof in the text for my logic course, and I'm wondering if someone could offer a hint or some help. The question is basically as follows. Show that if the decision problem for ...
5
votes
1answer
1k views

Difference between First Order Logic and Predicate Calculus

I see the two used interchangeably. Is one the subset of the other or are they both the same thing?
10
votes
1answer
628 views

Term rewriting; Compute critical pairs

I have tried to solve the following exercise but I got stuck while trying to find all the critical pairs. I have the following questions: How do I know which critical pair produced a new rule? How ...
2
votes
1answer
74 views

What can be concluded from a full application of resolution?

I know that resolution is refutation complete, but what can we conclude if a resolution procedure leads to a situation with no more chance to operate the resolution? Given a propositional formula ...
1
vote
0answers
75 views

Undecidability of an existential theory

$F[u, u^{-1}]$ is a ring that contains the polynomials in $u$ and $u^{-1}$ with coefficients in the field $F$. Some theorems (from https://math.stackexchange.com/questions/1382120/ft-has-undecidable-...
3
votes
1answer
27 views

Extension of Tarski's result on the decidability of reals

Due to Tarski's result, it is well-known that the first-order theory of reals $(\mathbb{R},+,\cdot,<,=,0,1)$ is decidable. I am working on a paper where I need an extension of this result. More ...