Questions tagged [first-order-logic]
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.
229 questions
0 votes
0 answers
33 views
Question on FOL limited to finite interpretations and standard name assumption
If I understand it correctly, in first-order logic, if $\phi(a,b) \models \psi(a,b)$, where $\phi$ and $\psi$ are first-order logic formulas and $a$ and $b$ are constants, then, $\phi(a,a) \models \...
- 559
0 votes
0 answers
61 views
Are the proposed truth tables for the rules correct?
I'm trying to propose truth tables for the following two rules which are originally defined on page 5 in this paper: Title: An abstract framework for argumentation with structured arguments Author: ...
- 101
1 vote
0 answers
99 views
Why Z3 loop infinitely for 2 simple axioms?
MY QUESTION IS "Why Z3 loop infinitely for 2 simple axioms?" Hi z3 falls infinite loop with the following 2 axioms: $(\forall x(\lnot(f_s(x)\hat{=}x))$ $(\forall x_1(\forall x_2((\lnot(x_1\...
- 111
0 votes
1 answer
98 views
confusion due to the difference of "terms" between FOL and SMT-LIB
In first-order logic (FOL), terms evaluate to values other than truth values, i.e., values of terms are neither true nor false. Reference: Chap. 2.1 from The Calculus of Computation By constrast, in ...
- 1
4 votes
1 answer
84 views
What is the corresponding lambda-calculus / proof terms of intuitionistic first order logic? (looking for references)
It is an oft-repeated result that lambda calculi correspond to logics. In particular, recall the following (approximate) relationships intuitionistic propositional logic ⇄ simply typed lambda ...
- 143
2 votes
1 answer
94 views
Is stable infinity required of theories combined with model-based theory combination?
In the paper "Model-Based Theory Combination" (1) by De Moura and Bjorner they present an alternative to the Nelson-Oppen method for theory combination. They first describe the Nelson-Oppen ...
- 205
2 votes
2 answers
106 views
Do stably-infinite theories exclude finite sorts?
Nelson-Oppen requires theories to be stably infinite. Meaning, that each theory allows extending models to have an infinite domain. A commonly mentioned counter example is that the theory of bit ...
- 205
0 votes
1 answer
183 views
Resolution on weakening rule by derived clause
How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule: $\frac{C} {C \vee D}$ (A clause $C$ is implied by $F$ if for ...
user150715
4 votes
0 answers
124 views
Extending Fagin's Theorem to the Polynomial Hierarchy
Fagin's Theorem (see Wikipedia and these lecture notes) states that there is an equivalence between second-order logic (SOL) formulas with existential quantifiers, and problems in NP. I was wondering ...
- 41
1 vote
0 answers
70 views
How do I prove relations of two CTL formulas?
If I have two CTL equations, how do I prove they're equivalent or that one implies the other? What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
- 346
3 votes
1 answer
225 views
how to do incremental construction of the minimal model in logic programming?
I was reading a book titled "Essentials of Logic Programming.", most parts of the book are easy to understand. but now having a problem with Theme 45: incremental constructions of the ...
- 1,034
0 votes
1 answer
184 views
Is any 2-CNF has 2-DNF representation?
I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
- 103
0 votes
2 answers
228 views
Can you help me in finding an algorithm that finds the first unique number in an array with lowest position?
I have the following problem to solve: Given a non-empty array A consisting of N integers, the task is to find the first unique number in the array. A unique number is defined as a number that occurs ...
3 votes
2 answers
180 views
'Someone' in first order logic
I have in the lectures a sentence in English, which I have to translate to First Order Logic. Someone who loves all animals loves all humans. Textbook solution: ∀x.(is_human(x) ⇒ is_animal (x)) ⇒ ∀...
- 33
0 votes
0 answers
107 views
Minimum DNF length of a conjuction of equivalences
Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses. I am puzzled on what approach to take -- whether to ...
- 109