Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [first-order-logic]

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

1
vote
1answer
19 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
0answers
9 views

Interpretation of free variables in theta-subsumption

How can one handle the free variable while using theta-subsumption to order the clauses according to the generality. I have three clauses: ...
0
votes
1answer
21 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
36 views

Convert FOL clauses to PROLOG

I am very new to PROLOG so it might be a very trivial question, but I absolutely have no idea how to solve it. There are 4 sentences I need to formulate into PROLOG code: All hounds howl at ...
1
vote
0answers
22 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
votes
0answers
26 views

how to prove $\Phi \vdash \forall x.R(x,x)$

I'm completely stuck in part 3 of below exercise, and dont even know how to begin proving this, other than writing all the premises
1
vote
1answer
12 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
64 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$...
1
vote
0answers
137 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 ...
1
vote
0answers
11 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
votes
0answers
18 views

Upper bound for a minimal resolution of unsatisfiable formula

Let $\varphi$ be a first-order-logic formula with $n$ literals ($X_1,...,X_n$). $\varphi$ is unsatisfiable. Now i want to know the upper bound of a minimal resolution of $\varphi$ resulting in the ...
1
vote
1answer
35 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
26 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
64 views

How do we translate first order logic's universal quantifier (the $\forall$) and the existential quantifier (the $\exists$) to Prolog?

I'm trying to convert some English statements to first order logic statements and I'm trying to use Prolog to verify the translations. My question is: how do I convert a first order logic statement (...
1
vote
1answer
50 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
41 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\...
3
votes
3answers
84 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
34 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?
4
votes
1answer
122 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 ...
1
vote
0answers
16 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
596 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
19 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
81 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 ...
2
votes
1answer
108 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
59 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, ...
0
votes
1answer
89 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
1answer
72 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 ...
18
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
2k 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
31 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
168 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 ...
0
votes
0answers
173 views

Inference with First Order Logic - Resolution with Forward Chaining

This is an example from the text book Artificial Intelligence: A Modern Approach, so I have the answer from the solution manual, I just don't fully understand how it was solved. ...
3
votes
2answers
78 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
228 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
41 views

Predicate calculus- meaning of the word “any”

In the following 2 statements - ...
3
votes
0answers
63 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
155 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
36 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
89 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
67 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
27 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
30 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
34 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
54 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
140 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
121 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
40 views

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

Does every 3CNF propositional formula has an equisatisfiable 2CNF propositional formula?
1
vote
1answer
72 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
59 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
63 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 ...