Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
25
votes
1answer
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 ...
17
votes
2answers
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 "...
41
votes
4answers
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 ...
1
vote
0answers
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 ...
18
votes
3answers
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 ...
8
votes
3answers
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 ...
15
votes
5answers
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. ...
17
votes
5answers
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 ...
4
votes
1answer
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 ...
44
votes
3answers
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 ...
-4
votes
3answers
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 ...
8
votes
2answers
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 ...
30
votes
4answers
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 ...
16
votes
1answer
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 $. ...
29
votes
3answers
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 ...
26
votes
5answers
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?
18
votes
1answer
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 ...
12
votes
6answers
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 ...
13
votes
6answers
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 ...
22
votes
1answer
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 ...
6
votes
3answers
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 ...
37
votes
2answers
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 ...
2
votes
2answers
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 ...
7
votes
3answers
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 ...
15
votes
3answers
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 ...
6
votes
2answers
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 ...
77
votes
5answers
3k views

Techniques for Reversing the Order of Quantifiers

It is well-known that in general, the order of universal and existential quantifiers cannot be reversed. In other words, for a general logical formula $\phi(\cdot,\cdot)$, $(\forall x)(\exists y) \...
6
votes
2answers
286 views

Practical applications of the Theory of Equality with Uninterpreted Functions (EUF)

In these days I'm reading the book Decision Procedures - An Algorithmic Point of View. Chapters 3 and 4 deal with the Theory of Equality with Uninterpreted Functions (EUF). The authors give 3 toy ...
3
votes
3answers
436 views

What does it mean for a language to have “order”?

In calculus, a polynomial has order $n$ if it contains terms that raise the unknown to a power $n$. I'm trying to figure out how this definition of "order" relates to the use of the same word when ...
29
votes
1answer
868 views

Is there a reasonable automated proof system for TCS theorems?

Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I ...
10
votes
2answers
382 views

Are there semi-decision procedures for this theory?

I have the following typed theory |- 1_X : X -> X f : A -> B, g : B -> C |- compose(g,f) : A -> C F, f : A -> B |- apply(F,f) : F(A) -> F(B) ...
20
votes
7answers
1k views

How can we know that formal methods work?

An important goal of formal methods is to prove the correctness of systems, either by automated or human-directed means. However, it seems that even if you can give a correctness proof, you may NOT be ...
14
votes
2answers
288 views

Cut-elimination for calculus with nats or other inductive datatype?

Does anyone direct me to a paper detailing a cut-elimination theorem for propositional intuitionistic logic, including an inductive datatype such as the natural numbers (lists or trees would be fine, ...
8
votes
2answers
393 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) ...
3
votes
2answers
2k views

What are “$\mu$-recursive functions” and $\mu$-calculus?

I saw in this question a reference to $\mu$-recursive functions or $\mu$-calculus as some computation model equivalent to Turing machines and $\lambda$-calculus. I know about these two but never heard ...
7
votes
2answers
772 views

An example of a totally computable function that is not definable in system T?

Could you give me an example of a totally computable function of type N × N → N that is not definable in System T? Thanks.
12
votes
2answers
482 views

What happens if we try to extract a witness but it actually does not exist from a term of existential type?

Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y)) in Martin-Lof's type theory, what's the value of w(t(0)), where ...
11
votes
1answer
701 views

NP vs co-NP and second-order logic

Assume that NP=co-NP and polynomial $p(x)$ bounds the length of the proof of unsatisfiability for a 3-CNF instance $x$. Then are there any results on what form any proof of unsatisfiability for $x$ of ...
12
votes
1answer
391 views

Can relativization results be used to prove sentences formally independent?

Is it possible to demonstrate that a sentence must be formally independent based on the fact that it is non-relativizing? In other words, are there examples of sentences in computability/complexity ...
10
votes
1answer
238 views

A direct sum theorem for Resolution clause space complexity?

Resolution is a scheme to prove unsatisfiability of CNFs. A proof in resolution is a logical deduction of the empty clause for the initial clauses in of the CNF. In particular any initial clause can ...
10
votes
1answer
369 views

Computational consequences of Friedman's (unprovable) Upper Shift Fixed Point theorem?

Harvey Friedman showed that there is a neat fixed point result that cannot be proved in ZFC (the usual Zermelo-Frankel set theory with the Axiom of Choice). Many modern logics are built on fixed ...
22
votes
6answers
765 views

Curriculum: Logical/Formal Methods in Security

At present I teach a small course (Four two hour lectures at the Masters level) on Logical Methods in Security, though the title Formal Methods in Security might be more apt. It covers briefly the ...
42
votes
4answers
3k views

Are there any proofs the undecidability of the halting problem that does not depend on self-referencing or diagonalization ?

This is a question related to this one. Putting it again in a much simpler form after a lot of discussion there, that it felt like a totally different question. The classical proof of the ...
17
votes
2answers
2k views

What do we know about restricted versions of the halting problem

(UPDATE: a better formed question is posed here as the comments for the accepted answer below show that this question is not well-defined) The classical proof of the impossibility of the halting ...
20
votes
0answers
493 views

Model-checking for three-variable logics and restricted structures

Denote the $k$-variable fragment of logic $L$ by $L^{(k)}$. The model-checking problem for a logic $L$ with respect to a class of structures $C$, denoted $MC(L,C)$, is the decision problem $MC(L,C)...
6
votes
1answer
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 ...
18
votes
1answer
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 ...
9
votes
5answers
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 ...
17
votes
5answers
398 views

Open or Interactive Constraint Satisfaction

In the past, I implemented coordination models using SAT and regular constraint satisfaction as the core workhorse in their engines. Continuing in this line of work, I would like to make the models ...
12
votes
0answers
217 views

Combinator logic and unification

Summary: if we are trying to use combinator logic to solve first-order logic type problems, is the best method to feed in free variables and use the standard first-order unification algorithm? In ...

1
6 7 8
9
10