Stack Exchange Network

Stack Exchange network consists of 175 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
votes
0answers
26 views

Is it possible to do forward-chaining in Prolog?

Prolog (or any logic programming system) actually acts as SAT solver, that returns the valid values for the variables that are mentioned in the query. It can also be used as theorem prover if one does ...
-1
votes
0answers
16 views

Is multi-theory approach the only way to do “higher-order” logic programming?

Lets consider logic program: likes(John, Vincent) loves(John, Ann) lusts(John, Tom) is_good(likes) is_good(loves) ~is_good(lusts) This program has 6 statements, ...
-1
votes
0answers
21 views

Predicate Logic - counter example when logical consequence doesn't hold?

I'm solving a predicate logic sentence. The logical consequence doesn't hold (i.e., I can't get to an empty bracket using the resolution method). I need to provide a counter example. Where do I even ...
1
vote
0answers
13 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 ...
1
vote
1answer
39 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 ...
0
votes
2answers
203 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 ...
3
votes
1answer
38 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 ...
0
votes
0answers
38 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 ...
0
votes
1answer
20 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 ...
5
votes
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 ...
2
votes
0answers
35 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 ...
2
votes
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 ...
2
votes
0answers
33 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 ...
0
votes
1answer
66 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)...
2
votes
1answer
152 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 ...
0
votes
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 ...
2
votes
1answer
39 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
0answers
32 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 [1], where it is also ...
1
vote
0answers
19 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, ...
0
votes
1answer
26 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
21 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
54 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 ...
1
vote
1answer
230 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
35 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
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 ...
1
vote
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$...
1
vote
0answers
151 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
vote
1answer
37 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
40 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) ...
2
votes
1answer
140 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
52 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
53 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
102 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
48 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
161 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
608 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
21 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
90 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
156 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
85 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, ...
1
vote
1answer
98 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
75 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
38 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
242 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
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
382 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}(\...