Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
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 ...

1
2 3 4 5
17