# Questions tagged [proof-theory]

Questions about analysis of proofs in theories

40 questions
Filter by
Sorted by
Tagged with
41 views

### The theory of definitions in first order logic

I'm looking for a clear and thorough treatment of the theory of definitions in first order predicate logic from a syntactic/proof theoretic point of view (as opposed to semantic/model theoretic point ...
187 views

### How do continuations represent negations (under the Curry–Howard correspondence)?

Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the ...
133 views

### An axiom for John Major's Equality

In the the standard library of Coq, there is the axiom: Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. Why isn't it provable? Can it be reduced ...
52 views

### Efficient transformation of clausal proof into resolution proof

Clausal proof is used to certify unsat results of SAT solvers. However the main theoretical results are on resolution proof (for instance, the non existence of a polynomial resolution proof for the ...
195 views

### Resolution vs Nondeterministic Search Problems

It is well known that each resolution refutation $\Pi$ for an unsatisfiable CNF formula $F = C_1\wedge C_2 \wedge ... \wedge C_m$ over variables $X$ can be translated in polynomial time (in the size ...
166 views

### Practical approaches to solving whether programs will halt

What kinds of systems are available that accept a certain program $P$ and attempts to figure out "the program does terminate" or "the program does not terminate" and output a proof of one or the other?...
395 views

343 views

### Looking for papers and articles on the Tarskian Möglichkeit

Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator: $\Diamond A =_{def} \neg A \to A$ (which he ...
1k views

### Are types propositions? (What are types exactly?)

I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
3k 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 ...
195 views

### Looking for papers and articles on higher-order sequent systems

I am looking for work on systems that are similar to K. Dosen's higher-order sequents ("Sequent Systems for Modal Logic", JSL 50). The only work that I am aware of is recent work by Iemhoff and ...
580 views

### Looking for papers and articles on modal substructural logics

I am looking for papers and articles on modal substructural logics-- not on the semantics of linear logic modalities, but on substructural logics augmented with standard modal operators, e.g. ...
2k views

### Curry-Howard and programs from non-constructive proofs

This is a follow up question to What is the difference between proofs and programs (or between propositions and types)? What program would correspond to a non-constructive (classical) proof of the ...
376 views

### About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.

Could anyone give an intuitive (not intutionistic) explanation of the correspondence of left introduction and elimination of implication in Sequent Calculus (SC) and Natural Deduction (ND) ...