# 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
0answers
30 views

### How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?

I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-...
1answer
13 views

3answers
145 views

### Can undecidability theorems be detected by a machine? [closed]

this question was originally written in mathoverflow, but a comment recommended me to rewrite it as a CS question. This is not a mathematically formalized question. I'm sorry for that but think it's ...
1answer
27 views

### Algorithm for automatic construction of natural deduction proofs

I was wondering if there exists any algorithm for automatic construction of nautral deduction proofs. I'm interested in propositional logic and first order logic. If there is no algoritm, can you ...
1answer
27 views

### Logical characterization of $NC^1$

Morioka in his 2005 dissertation  referenced "On Uniformity within $NC^1$" by Barrington, Immerman, and Straubing. Using the following statement: Every $\mathbf{NC^1}$-predicate is computed by ...
0answers
14 views

### How can I compute the most general unifier for these two expressions?

I have the following first order logic expressions: $f(g(a, h(b)), g(x, y)),~f(g(z,y), g(y, y))$ and I want to compute the most general unifier for them. If I follow the algorithm found on these ...
1answer
22 views

### List of all possible reasoning tasks - satisfiability and theorem proving only?

What is the exhaustive list of reasoning tasks? As far as I can understand, then any logical reasoning reduces to 2 tasks only: 1) satisfiability problem (finding the assignment of the variables) and ...
1answer
47 views

### MSO (Monadic second-order logic) Logic On Words

Let L be a language over $\Sigma = \{a,b,c\}$ that contains all words, where the length $|w|_b$ (number of all b's) has remainder 1 if divided by 3. MSO logic over words are definded as follow: I ...
1answer
81 views

### Is it possible to encode logical expression and interpret it with SQL?

Is it possible without any forms of eval or stored procedures to execute a query, which interprets logical expression, encoded in some way in a table (or two tables)...
1answer
273 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 ...
2answers
209 views

### The barbers paradox first order logic formalization

I tried to look on the site and while I found some similar questions, I did not find the first order logic formalization of the following sentence (the basic barber's paradox), so I wanted to ask if I ...
1answer
49 views

### Basic second-order logic example contains a mistake?

I'm reading the following course on second-order logic, by Péter Mekis : http://phil.elte.hu/mekis/sol.pdf . The course seems excellent, but I'm stuck on one of his first examples for showing the ...
0answers
34 views

### What is the computational complexity of the first-order theory of real arithmetic?

Tarski proved that the first-order theory of real-closed fields is decidable. Is the exact computational complexity known? The best upper bound I could find is EXPSPACE , where it is also ...
0answers
43 views

### Relational Algebra with only one operator?

There's a parlour game of inventing exotic operators for Relational Algebra, and thereby reducing the number of operators needed to be 'Relationally Complete'. A popular operator for this is 'Inner ...
2answers
2k views

### Why do ¬, ∀ and ∃ have the same precedence?

I thought the order of precedence of operators and quantifiers was arbitrary, but I don't really understand why those three have the same "strength" in relation to other operators (e.g., ¬ will have ...
0answers
41 views

### Ontology Editor or Something Else (in my case)? [closed]

Does there exist a system, e.g., software, an environment, a programming language, or the like, to represent knowledge and to reason with it, to query with, where the (descriptive) language used is at ...
1answer
43 views

### Terminology First-Order Logic

A graph $G$ is said to be a model of a first-order sentence $\varphi$ if $G$ satisfies $\varphi$. Now let $\varphi(x_1,...,x_r)$ be a first order formula with free variables $x_1,...,x_r$. What is ...
0answers
35 views

### Reference Request - Typed First-Order-Logic Book

There are many great references for computer scientists interested in untyped first order logic, such as Melvin Fitting's "First-Order Logic and Automated Theorem Proving" or John Harrison's "Handbook ...
1answer
155 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 ...
0answers
13 views

### KB implication vs and

i m doing KB from sentence to model. I m stuck on this sentence that say this : The packages stored in room1 are smaller than those stored in room 2. I m created this vocabulary Package X ...
1answer
40 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 ...
1answer
117 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 ...
0answers
28 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, ...
1answer
29 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 ...
1answer
24 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 ...
1answer
70 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 ...
0answers
40 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 ...
1answer
103 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 ...
0answers
156 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 ...
1answer
14 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 ...
2answers
69 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$...
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: ...
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 ...
1answer
38 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 ...
1answer
46 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) ...
1answer
179 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 (...
1answer
54 views

1answer
610 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 ...
1answer
23 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 ...
1answer
91 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 ...
4answers
372 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 ...
1answer
189 views