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
2
votes
1answer
163 views

Decidability of equivalence to existential formulas

I'm looking for an algorithm to decide if a given first order formula over a fixed vocabulary admits a logically equivalent existential one (i.e. a formula in prenex form where all quantifiers are ...
3
votes
1answer
44 views

Refutation in first order logic

Consider the following statement In FOL, we can reduce entailment checking to satisfiability checking: $S \models S' \iff S \land \neg S'$ is satisfiable (This proof strategy is called ...
2
votes
1answer
193 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 ...
2
votes
0answers
31 views

Superposition calculus: greater vs greater-or-equal

Bachmair and Ganzinger 1991, 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', specifies the criterion for using an equation as, by some appropriate ordering, ...
1
vote
1answer
40 views

Superposition calculus: Elimination of redundant atoms

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', section 5.2, 'Simplification and Deletion Techniques', page 17, 'Elimination of redundant ...
1
vote
1answer
29 views

Bachmair and Ganzinger, ordering of equations

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical ...
0
votes
1answer
300 views

Real world applications of first order logic

I study an AI course and we done some lectures about first order logic and the first thing that I was thinking is, what are the real world applications of first order logic and generally logical ...
2
votes
0answers
100 views

Why Modus ponens works with Horn clauses and Generalized Modus ponens requires definite clauses?

I am reading the Artificial Intelligence: A Modern Approach book and in the chapters about logic i noticed that in propositional logic the Modus ponens inference rule (used by the forward and backward ...
1
vote
1answer
154 views

Logical and non logical symbols and predicates

I am going through the text from "R.Brachmann and H.Levesque: Knowledge representation and reasoning". Here it has been described(in page 15) that there are two types of symbols : the logical symbols ...
1
vote
0answers
166 views

Does this Haskell code represent a decision procedure for a theorem?

The following is a natural language description of a first order theory from Worboys. Only Axiom 11 and the Theorem 4 are written in mathematical notation. Theory 1 Aland, Bland, Cland, and Dland are ...
1
vote
1answer
16 views

Why the given statement can't be expressed using predicates and quantifiers in the way described in details?

Suppose there is a statement - Some students in this class has visited Mexico. Solution given is: considering the universe of discourse for the variable $x$ consists of all the people. Our ...
1
vote
2answers
72 views

Must $x$ and $y$ be different in a statement of the form $\forall x \forall y \cdots$?

Given the following predicate formula $F$: $$\forall x \forall y [(\text{italian}(x) \Rightarrow (\text{winWC}(y) \Rightarrow \text{happy}(x))]$$ I am having trouble understanding whether $x$ and $y$...
2
votes
1answer
151 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: ...
2
votes
0answers
21 views

Can Description Logic be expressed by compiler type systems?

The Semantic Web defines standardised logic under the OWL DL standard. Programming languages such as OCamel and TypeScript support type inference and algebraic types. What are the difference between ...
1
vote
1answer
42 views

predicate logic proof of 2 numbers

For any two different numbers there is an number in between. I'm trying to write this in predicate logic and have no idea how to do it, since I need 2 variables X and Y? For all x there exists a y ...
-1
votes
1answer
74 views

predicate logic/binary relation help

(1) ∀x, y, z (x < y ∧ y < z → x < z) (transitivity) (2) ∀x ¬(x < x) (antisymmetry) (3) ∀x, y (x < y ∨ x = y ∨ y < x) (linearity) I need to give an example of a (nonempty) ...
1
vote
1answer
66 views

Are the definitions of recursively enumerate equivalent?

There are a couple of definitions of recursively enumerable, for example in Judah: $A \subset \mathbb{N}$ is called r.e. if there exist a $\Sigma^0_1$ formula $\varphi(x)$ such that $$A:=\{n \in \...
3
votes
0answers
56 views

A book introducing proof theory needed (many-sorted FOL, classical non-Gentzen calculus, satisfiability in partial algebras, induction)

We define a signature as a triple $$\Sigma\ =\ (S,F,\mathrm{type})$$ where $S$ is a set of sorts, $F$ a set of $n$-ary function symbols $f$ of the type $\mathrm{type}(f)$ $=$ $(M_1,\dotsc,M_n\...
4
votes
1answer
274 views

Logical characterization of P versus NP problem (and references for least fixed point logic)

Wikipedia says the following (and more) about the logical characterization of the P versus NP problem here: Thus, the question "is P a proper subset of NP" can be reformulated as "is existential ...
3
votes
3answers
370 views

Represent there are infinitely many in FOL

How to represent in first order logic the expression: "there are infinitely many" To be honest I'm confused and not even sure whether you can represent them in first order logic.
0
votes
1answer
408 views

How to convert statement with the existential quantifier to statement with universal quantifier?

How to convert the following statement with the existential quantifier to statement with universal quantifier? $\exists n. n>1\rightarrow x(n)\not=1$ Please give me some suggestion?
1
vote
0answers
17 views

Differentiate arguments in SPASS prover formula

I have a formula in FOL: $\forall x \exists y: B(x) \implies C(y)$ and in SPASS: forall([X], exists[Y], implies(B(X),C(Y))) I want to check the formula: $\exists x:...
3
votes
1answer
638 views

Resolution of Barber paradox

I am trying to prove using the resolution technique that the following two clauses are contradicting: $\forall_x Shaves(Barber, x) \iff \neg Shaves(x, x)$ $\exists_x Shaves(x, Barber)$ After turing ...
2
votes
1answer
30 views

Unclear logic notation for PFX program rules

I'm very new to this so please bear with me. I found this document describing the PFX language, a stack-oriented language where the instructions act on a stack and replace the arguments with the ...
4
votes
1answer
113 views

The equational theory of regular languages has no finite set of axioms for general alphabets

According to Redko the equational theory of regular languages with operations $+, \cdot, *$ over a single letter has no finite set of axioms. Why does this imply that it has no finite set of ...
1
vote
4answers
434 views

What is the point of (Compactness theorem in the) Overspill principle?

The principle (called a Löwenheim–Skolem theorem by Huth and Ryan) states Let $\phi$ be a sentence of predicate logic such that for any natural number $n \geq 1$, there is a model of $\phi$ with ...
3
votes
1answer
401 views

Trying to understand interpretation and denotation in FOL

I am going through the book "Knowledge Representation and Reasoning" by Brachman and Levesque. So an interpretation $ F $ is defined as a pair $ \langle D,I \rangle $ mapping from a set of objects $ ...
1
vote
2answers
141 views

The set of valid sentences in FO is not decidable as a consequence of rec. inseparability

Two given languages $L_1$ and $L_2$ are called recursively separable iff there exists a recursive languge $R$ such that $L_1 \subseteq R$ and $L_2 \cap R = \emptyset$. Now consider first order logic, ...
2
votes
1answer
91 views

Classical set theory and the existence of at least one set

As a student of mathematics I used to accept the argument that the existence of the empty set followed from the axiom schema of comprehension, so long as we could prove the existence of at least one ...
20
votes
4answers
5k views

Can proof by contradiction work without the law of excluded middle?

I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my ...
12
votes
5answers
3k views

Why does soundness imply consistency?

I was reading the question Consistency and completeness imply soundness? and the first statement in it says: I understand that soundness implies consistency. Which I was quite puzzled about ...
0
votes
0answers
48 views

Description logic representation

If Manufacturer manufactures electronic equipment, then manufacturer generates e-waste. I have generated the triple. However how to represent the if-then statement in DL? ...
0
votes
1answer
411 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 ...
4
votes
2answers
90 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
863 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
67 views

Predicate calculus- meaning of the word “any”

In the following 2 statements - ...
2
votes
0answers
133 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
226 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
45 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
153 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
99 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
59 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
71 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
383 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 ...
3
votes
1answer
137 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 \...
7
votes
3answers
4k views

Is resolution complete or only refutation-complete?

Going through some knowledge representation tutorials on resolution at the moment, and I came across slide 05.KR, no77. There it is mentioned that "the procedure is also complete". I think this ...
0
votes
1answer
67 views

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

Does every 3CNF propositional formula has an equisatisfiable 2CNF propositional formula?
5
votes
1answer
77 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 ...