# Questions tagged [lo.logic]

Computational and mathematical logic.

474 questions
Filter by
Sorted by
Tagged with
131 views

### Proofs for Implementation Statements

I've been struggling with understanding of the proofs showing that implementation statements are extensional. Basically I am referring to material described in Abstraction Classes in Software Design ...
115 views

### Implied Clause and Resolvent

(I posted this question on MathSE first, no answer, that is the reason why I come here.) Let $F$ be a 3-CNF formula on $n$ variables. A clause $c$ is implied by the formula if $F$ and $F \wedge c$ ...
541 views

### Constructively efficient algorithms without efficient correctness and efficiency proof

I am looking for natural examples of efficient algorithms (i.e. in polynomial time) s.t. their correctness and efficiency can be proven constructively (e.g. in $PRA$ or $HA$), but no proof using only ...
424 views

### Proofs in $S_{2}^{1}$

In a talk by Razborov, a curious little statement is posted. If FACTORING is hard, then Fermat’s little theorem is not provable in $S_{2}^{1}$. What is $S_{2}^{1}$ and why are current proofs not ...
404 views

365 views

### Inductive definition of ECTL*: how are recursive formulas forbidden?

In , the extended computation tree logic ECTL* is inductively defined as the propositional formulas over all E($A(F_1,..F_n)$), where E is the existential path quantifier and $A$ some Büchi ...
1k views

### Pointers for CS applications of logic

I'm a grad student in math with a solid background in logic. I've taken a year-long graduate course in logic together with graduate courses on finite model theory and another on forcing and set theory....
601 views

### Combinators for the Primitive Recursive Functions

It is well-known that the S and K combinators are Turing Complete. Are there combinators that suffice to yield (only) the primitive recursive functions?
694 views

### Free theorems, where?

I've found this webapp which lets you generate a free theorem for a given type. The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of ...
455 views

804 views

### “Guarded” negative occurrences in definition of inductive types, always bad?

I know how some negative occurrences can definitively be bad: ...
2k views

### Sum-of-squares proof system

Recently I have seen several articles on arxiv that refer to a proof system called sum-of-squares. Can someone explain what is a sum-of-squares proof and why such proofs are important/interesting? ...
465 views

### A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
833 views

### Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?

This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory. The post makes the claim of a future 'unification' between the the describing language of math, and the operation ...
132 views

### How to generalize a map of type for many operators?

I am formalizing the type system for a small language, and thus writing inference rules. Taking unary - operator for example, its entry may be a number as well as ...
122 views

### How to auto-derivate sequential iterative programs from a mathematical specification?

I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory. First, write down the formal specification as a Hoare triple and figure ...
4k views

### Understanding least-fixed point logic

To better understand a paper I'm trying to get a brief understanding of least-fixed point logic. There are a few points where I am stuck. If $G = (V,E)$ is a graph and  \Phi(P) = \{(a,b) \mid G \...
598 views

### Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?

I know that's impossible to decide $\beta$-equivalence for untyped lambda calculus. Quoting Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984).: If A ...
353 views

### How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, ...
293 views

### Intuition behind proof systems

I'm trying to under stand the paper On p-Optimal Proof Systems and Logic for PTIME. There is a notion called proof systems in the paper and I do not get the intution: $\Sigma = \{0,1\}$ ... We ...
194 views

### Temporal Logic and Access Control Models

What is the best way to describe the semantics of a new access control model?. I heard the temporal logic is the way to go. Is it true?
161 views

### Is the theory of asymptotic bounds finitely axiomatizable?

Let $F$ be the set of functions over real numbers. Consider the structure $M = \langle F, <, \leq, =, \geq, > \rangle$ where the $<, \leq, =, \geq, >$ are defined as asymptotic notions $o$,...