# Questions tagged [lo.logic]

Computational and mathematical logic.

474 questions
Filter by
Sorted by
Tagged with
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 ...
1k views

### Trace Equivalence vs LTL Equivalence

I am looking for an easy example of two transition systems that are LTL equivalent, but not trace equivalent. I have read the proof of Trace Equivalence being finer than LTL Equivalence in the book "...
4k 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 ...
58 views

### What Fuzzy techniques can combine conflicting quantified data?

I have been reading Fuzzy Belief Revision and trying to determine how the methods could be used to combine readings from conflicting sensors. For example, if one sensor reads 70 degrees and another ...
2k views

### Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
203 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 ...
603 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. ...
1k views

### Ambiguity and Logic

In automata theory (finite automata, pushdown automata, ...) and in complexity, there is a notion of "ambiguity". An automaton is ambiguous if there is a word $w$ with at least two distinct accepting ...
123 views

### Are there Belief Revision techniques for quantified data?

Are there Belief Revision techniques that aren't based solely in formal logic propositions? For example, if one agent believes the temperature for an area is 85 degrees and another believes the ...
3k views

### How do 'tactics' work in proof assistants?

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal ...
520 views

### Time-based mathematics or logic [closed]

The conventional systems of logic can only recognize or perform operations that transform or translate values in space. Ordinary logic treats time poorly through the necessity of translating all ...
331 views

### DATALOG references

What are the best references for self study in DATALOG? I am particularly interested in expressive power, complexity results, evaluation methods, extensions of DATALOG with negation etc. Are there any ...
3k views

### What are the differences between logical relations and simulations?

I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused ...
446 views

### Average-case tautologies/contradictions, beyond the random k-CNF model

It is well known that random $k$-CNF formulas over $n$ variables with $cn$ clauses are unsatisfiable (i.e. they are contradictions) with high probability, for sufficiently large constant $c$. ...
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 ...
1k views

### What is the difference between proofs and programs (or between propositions and types)?

Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?
3k views

### Prove proof irrelevance in Coq?

Is there a way to prove the following theorem in Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDIT: An attempt to give a brief ...
2k views

### Proof assistant for writing mathematics

I'd like to write mathematical proofs using some proof assistant. Everything will be written using first order logic (with equality) and natural deduction. The background is set theory (ZF). For ...
633 views

### What are practically computable properties of Labelled Transition Systems?

I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would ...
2k views

### Where is the proof that Coq + Excluded Middle is consistent

I've seen (and heard) it claimed that it is safe to add the classical axiom of excluded middle to Coq, but I can not seem to find a paper supporting this claim. The papers I see listed on the Coq wiki ...
1k views

### What is First-Order Rewritable (and FO-Query)?

I just wonder what FO Rewritable is, put an example to make it clearer for me. Also, I heard that a language that is FO Rewritable is very good, in what sense? It is said as follow: A class C of ...
3k views

### Axioms necessary for theoretical computer science

This question is inspired by a similar question about applied mathematics on mathoverflow, and that nagging thought that important questions of TCS such as P vs. NP might be independent of ZFC (or ...
524 views

### First order expression for functional dependency

I'm puzzled with functional dependency formula in first order logic. It is triggered by http://rjlipton.wordpress.com/2010/01/17/a-limit-of-first-order-logic/ where there seems to be a confusion ...
336 views

### Discharged hypotheses in ->Introduction

I have a question about page 9 in Proofs and Types. The given $\rightarrow$Introduction rule says that $A \rightarrow B$ can be deduced from $B$ if the deduction of $B$ contains an arbitrary number ...
593 views

### Theories which characterize classes of computational complexity

When reading the paper "An applicative theory for FPH" you can encounter the following passage: Considering theories which characterize classes of computational complexity, there are three ...
298 views

### Reference for checking primitive recursiveness

There is a theorem that states a function $f$ can be computed with a Turing-machine in time $O(g)$ with primitive recursive $g$ (of the length of input) iff $f$ is primitive recursive. Where can I ...
3k views

153 views

### Non-interesting numbers via resource-bounded properties?

There is an old joke about the smallest non-interesting number being interesting in itself (I have heard it attributed to Richard Hamming). This is then used to justify the argument that every number ...
662 views

### Techniques for showing non-derivability in logics and other formal proof systems

In proof systems for classical propositional logic if one want to show that a certain formula $\psi$ is not derivable one simply shows that $\neg\psi$ can be derived (although other techniques ...
963 views

### Writing universal recursive function [closed]

Is there a short explicit construction of an universal recursive function? All definitions I have seen involve numbering of Turing machines in some way, which is possible yet seems hard and ...