# Questions tagged [lo.logic]

Computational and mathematical logic.

464 questions
Filter by
Sorted by
Tagged with
187 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?
147 views

### Well-formedness condition for inductive types

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
479 views

### Can we distinguish strictly syntactic and semantic methods in programming language?

While discussion strong normalization proofs, this comment contrasts the "normal forms model" with "purely syntactic methods". This brings me back to a more basic question: can we still distinguish ...
337 views

### Natural theorems proven only “to high probability”?

There are plenty of situations where a randomized "proof" is much easier than a deterministic proof, the canonical example being polynomial identity testing. Question: Are there any natural ...
191 views

934 views

207 views

### Lower bounds for formulae sizes for addition

I am interested in the conversion of $\sum_{i=1}^n x_i = y$ to 3-CNF. Here $x_i$ is a binary 0/1 variable and $y$ is some positive integer. There are a number of practical methods for doing this, ...
239 views

4k views

### What is the logarithm or root operation in type-space?

I was recently reading The Two Dualities of Computation: Negative and Fractional Types. The paper expands on sum-types and product-types, giving semantics to the types ...
642 views

### Most important topics for a short introduction to Prolog

Suppose you were teaching an introductory course on logic as part of a TCS curriculum. Furthermore, suppose that you had one week (= two 90 minute lectures) to spare for introducing Prolog on the ...
871 views

### funsplit and polarity of Pi-types

In a recent thread on the Agda mailing list, the question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark. My understanding is that $\eta$ laws come with negative ...
Context: Kavvadias and Sideri have shown that the Inverse 3-SAT problem is coNP Complete: Given $\phi$ a set of models on $n$ variables, is there a 3-CNF formula such that $\phi$ is its exact set of ...