# Questions tagged [first-order-logic]

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

165 questions
Filter by
Sorted by
Tagged with
11 views

### Synthesis of the crisp programs from the Bayesian (probabilistic) programs?

https://arxiv.org/abs/2001.00805 is the article which is pointing towards the direction that the optimal policy of the reinforcement learning can be expressed as the Bayesian/probabilistic program (...
17 views

### What could be the bound of the number of elements of a models of a given first order sentence?

Sorry for the weird title. The Problem: Consider the first-order logic sentence φ≡∃s∃t∃u∀v∀w∀x∀yψ(s,t,u,v,w,x,y) where ψ(s,t,u,v,w,x,y,) is a quantifier-free first-order logic formula using ...
18 views

### Can full first order knowledge base be written as the single sequent in the sequent calculus?

The knowledge base of the first order logic essentially is single formula: conjunction of individual formulas (I guess, I am right). The sequent for the sequent calculus is the formula in the special ...
6 views

### Is it possible to write down every Prolog program+query as the sequent in the sequent calculus?

Prolog program P is set of Horn (definite) clauses, effectively it is the conjunction of implicational formulas. I guess that every Prolog program P with some query Q can be written as ...
23 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 ...
46 views

### General resolution in first order logic

Assuming you have a formula in first order logic like $$(\forall_x p(x) \land \forall_x q(x)) \rightarrow \forall_x(p(x) \land q(x))$$ (which seems valid?) Converting the formula to ...
26 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"...
40 views

### Combining Predicate Logic and BigO

I am a beginner to predicate logic and BigO and am having though time understanding the definition of BigO in terms of predicate logic in the picture attached. I particularly am unable to understand ...
14 views

### How to compute (partial) consequence set for premises of the first order logic?

I am playing with the Sequent Calculus Trainer https://www.uni-kassel.de/eecs/fachgebiete/fmv/projects/sequent-calculus-trainer.html . It is game with judgments, where each judgment consists from: 1) ...
33 views

### On satisfiability for 2-variable FOL being NEXPTIME-complete

Let $\mathbf{FO^2}$ be the fragment of first-order logic consisting of sentences with at most two variables and no function symbols. It is well known that satisfiability for $\mathbf{FO}^2$ is ...
32 views

### How to correctly negate a predicate bounded by some quantifiers?

this is a problem which was asked in GATE CS 2010. This is question statement: Q: Suppose the predicate F(x, y, t) is used to represent the statement that person x can fool person y at time t. which ...
10 views

### It is possible (and how to do) forward chaining (inference) in (standard) Prolog?

Forward chaining (inference) is an easy process that tries to deduct interesting consequences from some set of axioms/rules/premises. The hard thing is to focus on the deduction path that gives some ...
34 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-...
22 views

I have some basic confusions about the definition of the guarded fragment of first-order logic. Hopefully someone can tell me where I'm wrong. GF in FO is defined by: Atomic formulas, $x=y$ and $R(... 0answers 33 views ### Can numbers (not sets of numbers) in Linear Integer Arithmetic form a Boolean algebra? As far as I understood, Boolean algebra is just one of the many first-order theories (1). It has the signature$\{\sqcap, \sqcup, \neg, \bot, \top\}$and the axioms: associativity, commutativity, ... 3answers 154 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 53 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 29 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 24 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 54 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 ... 2answers 271 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 53 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 56 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 ... 1answer 24 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 ... 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 49 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 45 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 39 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 102 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 158 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 41 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 ... 0answers 46 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 30 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 31 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 25 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 138 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 ... 1answer 390 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 ... 0answers 67 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 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 70 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$... 0answers 160 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 ... 0answers 15 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 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 ... 1answer 53 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) ... 2answers 398 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 59 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 \... 0answers 55 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\...
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?