# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

821 questions
Filter by
Sorted by
Tagged with
11 views

28 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 ...
39 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)
39 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 ...
47 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 ...
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 ...
134 views

72 views

712 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 ...
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 ...
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 ...
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 ...
15 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 ...
37 views

### What is the theoretical result of flattening a list containing only itself?

Consider the following python code X = [None] X = X This has many fun properties such as X == X and ...
66 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 ...
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://...
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 ...