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
0
votes
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 ...
3
votes
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, ...
2
votes
2answers
394 views

Max() in Domain Relational Calculus

I was looking through my notes on domain relational calculus, and noticed an interesting result in a question about finding the most expensive pizza(s), given a pizza table with schema $\text{pizza}(\...
0
votes
2answers
46 views

Predicate calculus- meaning of the word “any”

In the following 2 statements - ...
2
votes
0answers
98 views

Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
5
votes
2answers
178 views

Undecidable predicate logic is decidable by people?

Logic in computer science (By Michael Huth,Mark Ryan, second edition, page 132) says Every φ can, in principle, be discovered to be valid or not, if you are prepared to work arbitrarily hard at ...
4
votes
0answers
39 views

Modern presentation of Ackermann's “Solvable Cases?”

Ackermann's book "Solvable Cases of the Decision Problem" discusses decidable instances of first order logic, particularly monadic logic, and so called "equality formulas". However, the book is from ...
4
votes
1answer
115 views

How logic programming (especially ASP) is related to the reasoning in (first-order) logic?

How logic programming (https://en.wikipedia.org/wiki/Logic_programming, especially answer set programming) is related to the reasoning in the (first-order) logic? Maybe logic programming can be ...
3
votes
0answers
86 views

How to translate lambda calculus into (first-order, modal) logic, is it possible at all?

It is possible (using formal semantics) to translate natural language sentences into lambda expressions. So, is it possible to translate those lambda expressions into some logic, e.g. into first-order ...
0
votes
0answers
28 views

Show the Invalidity of the sequence

∃x (P(x) → Q(x)), ∃x P(x) ⊨ ∃x Q(x) I am trying to find the invalidity of the following sequents. A = Set of natural number P(x) : x is odd Q(x) : x is not divisible by 2 What i don't understand ...
0
votes
1answer
35 views

Finding Models for a sequent

I am trying to generate models for the following sequent. $$\exists x \exists y \forall z (z = x \lor z = y)$$ What I have come up with is this. $$A= \{0,1\}$$ So in this model, for all the values ...
1
vote
1answer
40 views

Showing the following sequents are not valid

$\lnot \forall x P(x) \models \forall x \lnot P(x)$ $P(x) : x$ is divisible by 2 or $P(x) : x$ is a dog. or $P(x) can be anything. I want to show the following sequents are not valid ..Isn't the ...
2
votes
2answers
59 views

Any Non-trivial Logic System Defined with only Equality

Preface We can define a system of logic by conjunctions of rules that system must follow. For example, if we wanted to define transitivity of numbers: $$F_1: \forall a,b,c. a < b \land b < c \...
2
votes
2answers
216 views

Proving that a sentence in first-order logic is not valid

By the completeness of FOL, one can show that a sentence $S$ in FOL is valid, i.e. that it holds true in every model, by exhibiting a proof of $S$. Such a proof string is a certificate of the validity ...
2
votes
1answer
129 views

Why k- Vertex Cover is not in PTIME when it can be expressed in FO-logic

We can express property that graph has vertex cover of size at most k with first order formula: $$\exists x_1 \exists x_2...\exists x_k (\forall y \forall z (E(z,y) \ \rightarrow \ \bigvee_{1 \leq i \...
0
votes
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?
2
votes
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 ...
5
votes
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 ...
0
votes
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 ...
1
vote
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 ...
1
vote
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. ...
2
votes
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 ...
2
votes
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 ...
3
votes
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 ...
5
votes
0answers
131 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
545 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
124 views

First Order Logic : Predicates

I have a small problem with the first order logic, in particular, predicate logic Let us take this sentence as an example: ...
3
votes
1answer
117 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 \...
1
vote
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 ...
1
vote
2answers
329 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
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 ...
3
votes
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 ...
2
votes
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,...
3
votes
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 ...
1
vote
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 ...
2
votes
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 ...
1
vote
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 ~ \...
1
vote
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 ...
1
vote
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), ...
3
votes
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 ...
0
votes
2answers
334 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 $\...
1
vote
1answer
537 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 ...
2
votes
1answer
61 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 ...
0
votes
0answers
46 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
306 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 ...
0
votes
1answer
171 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 ...
3
votes
1answer
307 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 ...
22
votes
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 ...
4
votes
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 ...
1
vote
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?