Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
789
questions
1
vote
1answer
30 views
What is the theoretical result of flattening a list containing only itself?
Consider the following python code
X = [None]
X[0] = X
This has many fun properties such as
X[0] == X
and
...
2
votes
0answers
40 views
Understanding $\lambda \mu$-calculus in more programming way
I am learning $\lambda \mu$-calculus (self-study).
I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic ...
1
vote
0answers
45 views
Maximum number after AND operation sum [migrated]
You are given an array of N numbers say [A1,A2,⋯An]. Let us define a function F(x)=∑i=1 to n (Ai&x) where & is bitwise AND operator. We needs to find the number of different values of x for ...
0
votes
0answers
13 views
Set of inference and first-order resolution
In Robinson's first-order resolution, we're usually interested in reaching a contradiction $\bot$ from a set of clauses $\Gamma = \{C_1, ..., C_n\}$ where each $C_i$ is a set of first-order atoms. We ...
0
votes
0answers
27 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
15 views
Can we use Axiomitization to decide CTL*?
As the title says. There are axioms for CTL*, but can we use them to decide whether a formula is satisfiable? We can use the trick $p$ is satisfiable $\iff$ $\lnot p$ is not valid. My problem is that ...
1
vote
1answer
44 views
Substitution lemma for types
TAPL (page 549) proposes the following lemma in order to prove soundness of System F type system:
Substitution lemma for types:
$E, X, \Delta \vdash t: T \implies E, [X \mapsto S] \Delta \vdash [X \...
0
votes
0answers
26 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$ ...
2
votes
1answer
30 views
Unification Algorithm without Occur Check
I have been reading about Unification algorithm here https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm
. And I wonder about the importance of occur check.
I know ...
1
vote
1answer
31 views
Proving a certain primitive recursive function exists
Assume $f\colon ω × ω → ω$ is a computable function. How can we prove that there is a primitive recursive function $g\colon ω × ω → ω$ where the following holds:
$∀n [∃s(f(n, s) = 1) ↔ ∃k(g(n, k) = 1)...
0
votes
1answer
30 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 ...
3
votes
3answers
417 views
how to construct a formula with an opposite SAT value of another one
given a formula S (that is built of binary variables and "or", "not", "and" gates).
IS there a polynomial algorithim that builds S' that satisfies:
S' satisfied if and only if S doesn't satisfied.
...
5
votes
1answer
86 views
proving program equivalence
I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there ...
2
votes
1answer
28 views
Natural deduction: understanding bottom elimination (¬e)
I am new to natural deduction and upon reading about various methods online, I came across the rule of bottom-elimination in the following example.
I do not understand the step in line 10.
Upon ...
17
votes
11answers
5k views
Why do logic gates behave the way they do?
I am a Software Developer but I came from a non-CS background so maybe it is a wrong question to ask, but I do not get why logic gates/boolean logic behave the way they do.
Why for example:
...
3
votes
1answer
83 views
When can the coinduction hypothesis be used?
We can use the induction hypothesis when we are proving a property for a structure that is well-ordered. I am aware that there is a proof for this.
When it comes to coinduction, I'm confused.
One of ...
1
vote
1answer
20 views
For given reduction f, can show “if f(x) in 4NAE then x in 3SAT”, but not “if x is not in 3SAT then f(x) not in 4NAE”
Claim: $3SAT \le_p 4NAE $, where reduction $f$ is defined as such: given a 3CNF formula $\varphi$, add to each clause a new literal $z$ (where $z$ is same literal for each clause), and return new ...
2
votes
0answers
30 views
Compiling an impure language into a pure stack-based language
For a personal learning and fun project, I build an abstract virtual machine based on a stack. The instructions are simple and act on the top of the stack only. There are also stack operators such as <...
1
vote
0answers
20 views
Correctness of Simple Programs
For a homework assignment I am asked to provide claim sequences to verify that the given conditional does indeed satisfy its specification (to compute in r the absolute value of x).
...
0
votes
0answers
13 views
Verification conditions for Hoare
I am reading about Hoare logic but I don't really understand the verification conditions part for proving partial correctness.
What's happening between step 1 to 2? Why do we ignore the Q := 0 and ...
1
vote
1answer
22 views
Hoare Logic for Factorial
I came across this hoare logic for factorials but I don't quite understand it. We multiply F and X but we're not adding up all values of F so how do we get the sum/factorial at the end?
Precondition: ...
2
votes
0answers
33 views
Large Conjunctive Normal Form Examples
I'm currently learning about conjunctive normal form in a course on logic for Computer Science. I was reading the Wikipedia entry on the subject and encountered this:
Typical problems in this case ...
1
vote
0answers
28 views
How is it possible that an equational theory be terminating?
I'm a bit tripped up by this fundamental notion of an equational theory with respect to how we can possibly get termination if we have that we can always orient a set of equations either right to left ...
1
vote
1answer
17 views
Injectivity not required for unification algorithms?
When learning about a general unification algorithm, we learned the rule decompose, which states unifying
$$G \cup \{f(a_0,...a_k)=f(b_0,...,b_k)\} \Rightarrow G \cup \{a_0=b_0,...a_k=b_k\}.$$
The ...
1
vote
1answer
18 views
Why does the substitution {x/f(y), y/z} work this way?
There is an example of applying a substitution to an expression, and I am having a problem with it.
Let $\theta = \{ x/f(y), y/z \}$, and $E=p(x,y,g(z))$,
then $E\theta = p( f(y),z,g(z) )$.
Why is $...
2
votes
1answer
31 views
Definition of 2-CNF (a.k.a Krom) formula
In my lecturer's notes, the following definition for a 2-CNF wff is given:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals.
However, there is ...
1
vote
0answers
24 views
Logic minimization via 2 inputs NOR gates: Is it monotone w.r.t to adding a minterm?
notation: $x+y:=\mbox{OR}(x,y)$, $\bar x:=\mbox{NOT}(x)$, $xy:=\mbox{AND}(x,y)$, 1:=TRUE, 0:=FALSE.
Let $f$ be a Boolean function of $n$-variables, i.e. $f: \{0,1\}^n \to \{0,1\}$.
minterm:= any ...
2
votes
1answer
41 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
55 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
27 views
Is Event Calculus applied for program verification?
Recently I've read wiki page about Robert Kowalski (Prolog author) and stumbled upon interesting concept of Event Calculus. The wiki article mentions only few applications of this logical language. I ...
1
vote
1answer
34 views
What is Herbrand interpreration and model?
I was reading the book "Foundations of Logic Programming" written by J.W. Lloyd. In the book, there were definitions of interpretation and model, and when it comes to herbrand interpretation and model,...
0
votes
0answers
26 views
Prove that exists PARITYn fuction with size O(n^2)
Have to find Boolean circuit formula that solves PARITYn problem with complexity O(n^2)?
(Function PARITYn(x1, . . . , xn) is equal to 1 if and only if the number of variables x1, . . . , xn equal ...
5
votes
1answer
84 views
How come correctness proofs aren't tautological?
Consider the following function on binary trees, which is supposed to tell whether a given int is a member of a binary tree t:
<...
0
votes
1answer
34 views
Representing a sentence using propositional logic
I am confused regarding a propositional logic representation of a sentence.
Please note that this sentence is not realistic:
"A person who is male (M) is smart (S) if he is tall (T), but otherwise ...
0
votes
0answers
51 views
How to show that a partial function is recursive?
I try to prove that this function is recursive:
$$f(x_1,x_2)= \begin{cases}
2x_1-x_2 & \text{if $x_1 \geqslant \sqrt{x_2}$} \newline
\bot & \text{otherwise}
\end{cases}$$
I think that I need ...
1
vote
0answers
14 views
Is true * true = true in Separation Logic?
I am trying to show that the following interference is unsound in terms of Separation Logic:
$$
(p_0 \implies p_1) \implies ((p_0 * q) \implies (p_1 * q))
$$
I came up with the following values for ...
1
vote
1answer
43 views
What algorithms for unification over (multidimensional) array terms?
I am looking for references on implementing unification over multidimensional array terms.
Are there specialized unification algorithms for those cases? I wasn't able to find satisfactory literature ...
2
votes
2answers
62 views
Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$
I am new to LTL and I am trying to understand how it works. My question is: is there such $\sigma$ that:
$ \sigma \models [\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)]$
I know ...
0
votes
0answers
30 views
Formalizing “dual-time” temporal logic
I am interested in modeling a discrete temporal logic based on music, where there are two metrics of time, beat and seconds, (call them B and S). The constraints on what constitutes a syntactically ...
1
vote
0answers
84 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 ...
0
votes
0answers
21 views
In what sense the computer program (Turing machine) can be considered as the complex system and its IIT Phi can be measured and improved?
I am reading https://global.oup.com/academic/product/a-world-beyond-physics-9780190871338?cc=us&lang=en& about one approach of complex systems' theory for the emergence of the life. It is ...
2
votes
0answers
21 views
Deciding Intuitionistic Logic via QBF
I want an algorithm to decide whether a theorem holds in propositional Intuitionistic logic ($IL$). We know $IL$ is $PSPACE$-complete, so we should be able to reduce $IL$ to $QBF$.
In Literature i ...
0
votes
2answers
168 views
Does the callback concept of programming have any basis in computer science?
Although I seriously code with computer languages in general since 2010 and as an amateur programmer with programming languages in particular since 2015 (primarily Bash and JavaScript imperative ...
0
votes
0answers
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 (...
0
votes
0answers
28 views
Bounds on the size of the universe of a model for an FO-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 ...
1
vote
0answers
34 views
Proof strategy to show that an algorithm cannot be implemented using just hereditarily terminating procedures
I am taking my question here from there. Consider the following scenario:
You are given a fixed programming language with no nonlocal control flow constructs. In particular, the language does not ...
0
votes
0answers
14 views
Is the standard terminology “logic operation” or “logical operation”?
I've heard both terms "logic operation" or "logical operation" used. Is either more common?
2
votes
1answer
150 views
Is it possible to prove Tarski's Undefinability theorem from Turing's Halting Problem?
In the Wikipedia page for Turing's Halting problem, they mention that you can prove Gödel's First Incompleteness theorem from it. This is the relevant quote:
Assume that we have a sound (and hence ...
1
vote
1answer
26 views
Simplifying a logic function using Boolean algebra
Consider this Logic function : D = A B C + A B’ C + A’ B’ C + A B C’ + A’ B C’ + A B’ C’ I am trying to simplify it using Boolean algebra , I am stuck in this step : D= AB +B'C+ A’ B C’ + A B’ C’ So ...
2
votes
2answers
70 views
diagonal lemma and the negation function
Carnap's diagonal lemma asserts that for every computable formula f, accepting a natural number as argument and resolving to {false,true}, there exists a logic sentence s for which:
s $\...
