# Questions tagged [lo.logic]

Computational and mathematical logic.

471 questions
Filter by
Sorted by
Tagged with
1k views

### Homotopy type theory and Gödel's incompleteness theorems

Kurt Gödel's incompleteness theorems establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic". Homotopy Type Theory provides an alternative ...
330 views

### Equational Logic and First Order Predicate Logic

I am interested in using Equational Theories (ET) together with Equational Logic (EL) found in algebraic specification languages such as CafeOBJ . I wish to use ET+EL to represent and prove sentences ...
342 views

### What is logic programming and does it really add anything new to the logic?

I am acquinted with the basics of such notions as logic programming, monotonic and non-monotonic reasoning, modal logic (especially dynamic logic) and now I am wondering - does logic programming ...
193 views

### Decidability of inductive invariant existence in Presburger arithmetic

Problem: Consider a finite number of control states (including an "initial" and a "bad" state), a finite number of integer variables, and for each ordered pair of states a transition relation ...
468 views

### “Correctness” of type theory

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one? When type ...
282 views

### Example of where violation of strict positivity condition in inductive types leads to inconsistency

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?
475 views

### Good description of Calculus of Inductive Construction

I want to learn more about Calculus of Inductive Constructions. What can you recommend to read on this topic? All the materials which I found are either in French or too basic (the Coq'Art book). The ...
197 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?
175 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. ...
523 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 ...
362 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 ...
198 views

1k views

### Start learning proof complexity

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, ...