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 [1], 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$,...