Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
807
questions
-1
votes
1answer
53 views
1
vote
1answer
37 views
Universal Quantifiers in QBFs
I've been looking into reductions to/from the TQBF language and have managed to get stuck on something that is almost certainly not true (or, if it is true I'm missing a significant computational cost ...
-2
votes
1answer
30 views
Lambda calculus simplification excercise
Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem.
(λx.λy.yx)z (λw.w)
I am lost with this.
if anyone could lead me in ...
0
votes
0answers
22 views
Two variants of Fredkin gate
Sometimes two outpus of Fredkin gate are swapped when constant bit is 0, sometimes when it is 1. What variant is right or more modern? If it was conscious decision to change behavior what was ...
1
vote
0answers
20 views
In theory, should neuromorphic computers be more efficient than traditional computers when performing logic?
There is this general sentiment about neuromorphic computers that they are simply "more efficient" than von Neuman.
I've heard a lot of talk about neuromorphic computers in the context of ...
0
votes
1answer
22 views
Represent a DNF formula as a multivariate linear formula?
Lets say I have the following DNF: (x or y) and (z or i) / $(x\lor y)\land(z\lor i)$
How do I convert that into a polynomial form?
5
votes
1answer
30 views
Test two LTL expression trees for equivalence
Is there an algorithm on how to check if two LTL expressions (represented as binary trees) are semantically equivalent? Since there are many smaller equivalences such as
$a\Rightarrow b \equiv \neg a \...
0
votes
0answers
20 views
Building an ALU on nandgame's website
I'm working on nandgame's website found here. I'm working on the ALU and here is an image of my implementation:
My Implementation:
And I compared it to this website's solution:
Solution
However when ...
2
votes
0answers
37 views
Can HOL be simulated in the CiC?
I was wondering if HOL (higher-order logic) can be simulated in the Calculus of Inductive constructions (CiC)
2
votes
1answer
32 views
What were the shortcomings of Robinson's resolution procedure?
Paulson et alii. From LCF to Isabelle/HOL say:
Resolution for first-order logic, complete in principle but frequently disappointing in practice.
I think complete means they can proof any true ...
0
votes
0answers
46 views
Is a or free SAT formula NP complete?
Let $L$ be the languague which contains all satisfiable formulas which do not have the or symbol $\lor $.
Or more precise $$L=\{\phi | \phi \text{ is a satisfable formula which is only using the ...
1
vote
0answers
40 views
Is there a way to simplify redundant conditionals?
For example if I've this:
if a == false then return true else
if a == true and b == false return true else
if a == true and b == true then return false
can be ...
3
votes
1answer
130 views
How many clauses are required for SAT to be NP-hard in CNF formulas?
It is not hard to see that SAT for a CNF formula with $n$ variables and a constant number of clauses can be solved in polynomial time. On the other hand, it is not hard to see that a CNF formula with $...
0
votes
1answer
41 views
How are prime implicates of HORN-Formulas defined?
I'm confused about the definition of prime implicates in Horn formulas.
For example in the paper of Kira 2012 on page 109 it is stated:
Now in the paper of Boros 2010 on page 82 the following ...
0
votes
1answer
33 views
Equivalence of Horn formulas tractable?
Assume I have two Horn formulas $\phi_1, \phi_2$. Horn formulas are CNF formulas so that each clause has at most one unnegated literal. For example:
$x_1 \wedge (\neg x_1 \vee \neg x_2 \vee x_3 )\...
2
votes
2answers
69 views
Equivalence of Krom formulas tractable?
Assume I have two Krom formulas $\psi_1, \psi_2$. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, $\...
0
votes
0answers
48 views
Note down the possible states in a truth table
You are required to automate the control of the water tank in your home. There are two water
contact sensors that turn to a TRUE state when in contact with water and a FALSE state when not.
Sensor $1 (...
4
votes
1answer
706 views
Question on the “Tutorial implementation of dependently typed lambda calculus”
I have a slight technical struggle with this marvelous tutorial. On page 5 the tutorial talks about typing rules for Simply Typed Lambdas and presents following judgement as derivable via rules on ...
0
votes
1answer
40 views
Consistent theory based on L and not(A->A) is a theorem
I am working on this problem in which I have a theory $T$ based on language $\mathcal{L}$ and the only information we have is that T is consistent and $\vdash \lnot(A \rightarrow A)$. Given this ...
1
vote
0answers
23 views
Impredicativity example in HOL
From these notes pages 37-38. In HOL, I'm giving the task of proving:
$\vdash \forall x^T. \forall y^T. (=_T x^T y^T) \implies (=_T y^T x^T)$
applying forall and implication introduction and the ...
0
votes
0answers
21 views
What is the best way to identify highly performing groups?
I am currently working on a project that involves sorting people into groups based on their ability to work well with others.
While it is a bit of a simplification, I have a problem that is ...
2
votes
1answer
14 views
Circuits and formulas for Clique
Is it correct to say that the Clique Problem is in $P$ iff there exists a family of Boolean circuits $C$ to decide Clique whose sizes are bounded by a polynomial? And based on this question, does that ...
1
vote
1answer
36 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
...
3
votes
0answers
63 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 ...
0
votes
0answers
16 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
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
16 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
50 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
35 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
32 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
31 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
419 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
89 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
35 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
85 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
23 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
23 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).
...
1
vote
1answer
26 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
34 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
29 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
18 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
20 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
42 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
50 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
28 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 ...
