# Questions tagged [lo.logic]

Computational and mathematical logic.

493 questions
Filter by
Sorted by
Tagged with
53 views

### Is there a fundamental link between Nash's equilibrium and Turing's halting problem?

Since Nash equilibrium exists, is there a computational analogue of this equilibrium point? I am trying to approach Nash equilibrium from computational point of view to see if the equilibrium point ...
384 views

### Incomplete basis of combinators

This is inspired by this question. Let $\mathcal{C}$ be the collection of all combinators which only have two bound variables. Is $\mathcal{C}$ combinatorially complete? I believe the answer is ...
4k views

### How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
86 views

### Where does "Quine's Method" in propositional logic originate?

Hein (407-408) states that Quine's method "...uses these (14) properties together with basic equivalences to determine whether a wff is a tautology, a contradiction, or a contingency." The ...
54 views

### Is relativization statement-dependent or proof-dependent?

I'm relearning some computability theory, and have encountered the idea of relativization of results to arbitrary subsets of $\omega$ and the subtlety of figuring out what the correct relativized ...
146 views

### Constructive Strong Normalization of the Extended Calculus of Constructions

The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
431 views

### Is there a good notion of non-termination and halting proofs in type theory?

Constructive type theory with its basic interpretation under the curry howard correspondence consists only of total, computable functions. In the literature, some has been said on using "computational ...
276 views

### How to use Prop from UTT in Agda

In Ulf Norell's thesis he mentions that Agda is based on Luo's UTT. However, I can't find a way to use Prop there. Is there any way to do so?
148 views

### Alternatives to Normalization by Evaluation

Reading about lambda calculus I got the impression that normalization is evaluation. So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel). ...
63 views

### Linear Integer Arithmetic Satisfiability with Three Literals [closed]

I'm stuck on trying to find an unsatisfiable conjunction of the form $a \wedge b \wedge c$ where: $a \wedge b$ is satisfiable $a \wedge c$ is satisfiable $b \wedge c$ is satisfiable $a, b, c$ are ...
82 views

### Boltzmann sampling for containers/dependent polynomials?

I’d like to randomly sample from dependently-typed data structures. Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials?
252 views

### Proof and computational complexity

I couldn't find documents elaborating on this: if the Curry Howard correspondence is to be interpreted as establishing a strong relation between proofs and programs, should there not be a strong ...
94 views

### Is unary $\Pi_2$-SUBSETSUM coNP-complete?
Consider the following problem: for given integers $a_1, \ldots, a_{2n}$ and $A$ that are given in unary representation define is it true that for every $S \subseteq \{1, ..., 2n \}$ such that \$|...