Questions tagged [first-order-logic]

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

45 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
6
votes
0answers
176 views

On the Turing Completeness of First Order Logic

It is well known that in Descriptive Complexity Theory FO is equivalent to AC0. However, this accepts a couple of a theory and a string <T,s> iff the ...
5
votes
0answers
33 views

Do FOL theorem provers accept axiom schemata?

Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata? I looked in the Vampire "manual" briefly,...
5
votes
0answers
134 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 $...
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 ...
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\...
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 ...
3
votes
0answers
79 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 ...
2
votes
1answer
64 views

Natural deduction proof: distributivity of existential quantification

In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic: $(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,...
2
votes
0answers
65 views

Sample applications based on First Order Logic

I often hear about benefits of FOL, but I wonder what are some of its real world applications? Could someone please provide samples/case studies of applications of FOL that address real world ...
2
votes
0answers
28 views

How to prove following two statements are equivalent in Hilbert System?

statement 1: $Γ$ is satisfiable implies $Γ$ is consistent. statement 2: If $Γ$ derives $α$ then $Γ$ entails $α$. I can easily prove statement 1 from 2 , but not 2 from 1 (without using strong ...
2
votes
0answers
45 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 ...
2
votes
0answers
64 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 ...
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, ...
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 ...
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 ...
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, ...
2
votes
0answers
29 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
2
votes
0answers
60 views

Completeness and first order logic with Least fixed point operator (LFP)

Is there any result about the extension of first order logic with least fixed point operator, being complete (as logic in general on infinite structures too) or not? In other words does the Goedel ...
1
vote
0answers
34 views

Help me understand whether these critical pairs are joinable

I have the following TRS $R$: $$ l_1 = f(g(x)) \to f(x) = r_1 \\ l_2 = g(f(y)) \to g(y) = r_2 $$ I want to know if $R$ is confluent, and whether $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$. I have ...
1
vote
0answers
12 views

What is the space-complexity of a boolean first-order query?

I have the intuitition that, if we implement a (space-efficient) boolean first-order query solver, the amount of consumed memory should depend on the data size (i.e., it should not be constant). ...
1
vote
0answers
47 views

How to write “∀x.F(x)” for “F(x)=λx.Φ(x)” in one expression (sequel from question about “∀(λφ. (φ x m→ φ y))”?

This question is sequel from How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"? which further explains the notation and context. So - I have anonymous Boolean-valued ...
1
vote
1answer
40 views

Z-Specification = Routes

Im trying to make an invariant for this Z schema about routes. 1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
1
vote
0answers
111 views

Proving a first order logic theorem in equational logic with a term rewriting system

I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean ...
1
vote
0answers
53 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
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
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:...
1
vote
0answers
153 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
0answers
177 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 ...
1
vote
0answers
35 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
0answers
48 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 ...
1
vote
0answers
178 views

Proving the following chain of implications

I'm struggling with a proof in the text for my logic course, and I'm wondering if someone could offer a hint or some help. The question is basically as follows. Show that if the decision problem for ...
1
vote
0answers
75 views

Undecidability of an existential theory

$F[u, u^{-1}]$ is a ring that contains the polynomials in $u$ and $u^{-1}$ with coefficients in the field $F$. Some theorems (from https://math.stackexchange.com/questions/1382120/ft-has-undecidable-...
0
votes
0answers
15 views

A necessary condition for a relation to be in 2NF but not in 3NF is that some non-prime attribute must be determined by a non-prime attribute

I will state the complete question now, since it did not fit in the title. Is the statement given below correct? A necessary condition for a relation to be in 2NF but not in 3NF is that some non-...
0
votes
0answers
14 views

Modal logic equivalent to two-variable first-order logic?

It is well-known that many modal logics can be viewed as fragments of $FO^2$, i.e. two-variable first-order logic. But is there a modal logic that is not a fragment, but is expressively equivalent to $...
0
votes
0answers
18 views

Is Inductive Logic Programming approach applicable to general theories (not just sets of Horn clauses)?

Inductive Logic Programming (https://en.wikipedia.org/wiki/Inductive_logic_programming) find hypothesis theory H for background theory B and set of examples E. ILP algorithms and implementations ...
0
votes
0answers
28 views

Situation calculus: how to find pre-conditions in 15-puzzle game?

I have been working on finding the preconditions for a situation calculus example for some time now. This example is called the game "15-puzzle" where you can find a discription here https://...
0
votes
0answers
30 views

Show that exist a finite set of clauses F in first-order logic that Res*(F) is infinite

I'm kind of desperate at this point about this question. A predicate-logic resolution derivation of a clause $C$ from a set of clauses $F$ is a sequence of clauses $C_1,\dots,C_m$, with $C_m = C$ ...
0
votes
0answers
34 views

Abstract syntax tree: expression->operation->lhs|rhs vs expression->lhs|operation|rhs - what should I take into account in decision?

I am trying to build class hierarchy for the abstract syntax tree of First Order Logic as specified in the grammar https://github.com/antlr/grammars-v4/blob/master/fol/fol.g4 (ANTLR parser generator). ...
0
votes
0answers
30 views

Is FOL representation of probabilistic assignment statement correct?

For instance, $x = x + 1[0.3]x+2$ sets $x$ to $x + 1$ with probability $0.3$ and to $x+2$ with probability $0.7$. If I use notation used in the paper "An Analysis of First-Order Logics of Probability"...
0
votes
0answers
35 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-...
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
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
0answers
115 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 ...
0
votes
0answers
88 views

What does an = sign with an x beneath it mean?

I am studying for a test in Logic right now, and saw the symbol $\underset{x}{=}$, which is used like this: $I \underset{x}{=} I'$. I've seen it in the solutions of questions like this one: Prove ...
-3
votes
1answer
71 views

Is this formula valid?

is this formula valid ??, if it is not what interpretation could i use ? (∀ x: P(x) -> ∀ x: Q(x)) -> ∀ x: (P(x) -> Q(x)). PS : i know that the other implication is valid.