Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
6
votes
1answer
386 views

Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus

I'm trying to work through two (non-assessed) class-work questions and am stuck on a question that seems similar to one I could do. The first question was to prove that there does not exist a $\...
4
votes
2answers
348 views

Parametric equation in pi-calculus

This is the first time I ask a question on cstheory, so I am very sorry for my english. I have a (maybe very trivial) problem when trying to find a well-form representation for a root of a recursive ...
8
votes
2answers
283 views

Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages)

I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, ...
9
votes
2answers
424 views

Do good PCPs for NP give us good PCPs for the entire polynomial hierarchy?

The PCP Theorem states that every decision problem in NP has probabilistically checkable proofs (or equivalently, that there exists a complete and quasi-sound proof system for theorems in NP using ...
13
votes
1answer
450 views

Lambda-Calculus terms that reduce to themselves

In my continuing quest to try to learn lambda calculus, Hindley & Seldin's "Lambda-Calculus and Combinators an Introduction" mentions the following paper (by Bruce Lercher) which proves that the ...
5
votes
3answers
707 views

Why does predecessor(zero) need to be zero in Church numerals?

My question may be similar to: Why naturals instead of integers?, but it is more specific. I am trying to learn lambda calculus. All the books make a big deal about how it was necessary that ...
17
votes
0answers
347 views

Descriptive complexity of communication complexity classes

It is well known that some major complexity classes, like P or NP, admit a full logical characterization (e.g NP = existential 2nd order logic by Fagin's theorem). On the other hand, one can also ...
18
votes
4answers
773 views

Automated theorem proving in linear logic

Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction? Where can I read more about automatic theorem proving in these ...
18
votes
2answers
758 views

How many tautologies are there?

Given $m, n, k$, how many of $k$-DNFs with $n$ variables and $m$ clauses are tautology? (or how many $k$-CNFs are unsatisfiable?)
7
votes
2answers
822 views

Closed term and alpha-conversion

In the simply-typed lambda calculus, do we ever need alpha-conversion in a small-step call-by-value reduction of a term that is closed? The evaluation rule that uses substitution is: $(\lambda x.t_1)~...
12
votes
1answer
416 views

Barendregt's proof of subject reduction for $\lambda2$

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types). The last step of the proof (page 60), says: "and hence by Lemma 4.1.19(1), $\quad\Gamma,x:\rho\...
-1
votes
1answer
607 views

How to prove a proof is correct

A one-line proposition $A$ can generate a 100-page proof $p(A)$. Since the proof is very long, it's highly suspectable that there is a mistake in it, which cannot be found out even after careful ...
16
votes
3answers
959 views

Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
6
votes
1answer
173 views

converse relationship between the cut rule and the identity axiom

On page 30 of "Proofs and Types" by Girard, Taylor, and Lafont, it is claimed that that the identity axiom for sequent calculus: C ├ C has a converse relation with the cut rule: $$\frac{\vec{A} \...
4
votes
2answers
151 views

finding constantness of a term

Let $S$ be a multisorted algebraic signature with function symbols $f_0, f_1, \ldots$. For every $i$, I partially know “constantness” of $f_i$. (I have no precise definition of constantness yet.) ...
5
votes
0answers
195 views

Logic capturing automorphism-invariant $\mathsf{AC^0}$ properties

Q1. Is there a logic that is computable in polynomial-time which contains all order-invariant properties computable in smaller classes like $\mathsf{AC^0}$ (or $\mathsf{TC^0}$)? Motivation As you ...
18
votes
4answers
3k views

What's the point of $\eta$-conversion in lambda calculus?

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda ...
7
votes
2answers
301 views

Simple model of computation with homoiconicity

Is there a simple model of computation with homoiconicity? It would also be nice if, like beta reduction in lambda calculus, every step in execution yields a new valid program. Besides the lack of ...
7
votes
1answer
1k views

How to use induction without Fixpoint definition in Coq?

I want to verify a program written in C. I am using Jessie to translate the (pre/post)conditions of the program to Coq. In Coq I will make a proof. Sometimes I need recursive definitions. ...
15
votes
2answers
408 views

Proof theory of biproducts?

A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts? Perhaps the best-known example is the ...
18
votes
1answer
701 views

A topological space related to SAT: is it compact?

The Satisfiability problem is, of course, a fundamental problem in theoretical CS. I was playing with one version of the problem with infinitely many variables. $\newcommand{\sat}{\mathrm{sat}} \...
6
votes
1answer
339 views

What is an unambiguous language in the sense of Schützenberger?

I'm reading Thomas Wilke's survey on the connections between Temporal Logic and finite automata, finite semigroups and first-order logic. In Theorem 6 (by Kamp), the fragment $\mathrm{TL}[\mathsf{F},\...
8
votes
1answer
150 views

Time/Space Requirements of Verifying or Falsifying a First-Order Statement

Though L.Berman proved that the problem of verifying or falsifying any first-order statement about real numbers that uses addition and comparison but not multiplication is in EXPSPACE. Has it been ...
24
votes
4answers
2k views

Starting SAT solver papers

I want to make a first SAT solver. I know the SAT competition and the SAT conference, and there are just so many papers on this subject. I'm a starter, an overwhelmed starter. Where should I begin? ...
37
votes
3answers
5k views

Extended Church-Turing Thesis

One of the most discussed questions on the site has been What it Would Mean to Disprove the Church-Turing Thesis. This is partly because Dershowitz and Gurevich published a proof of the Church-Turing ...
-3
votes
1answer
319 views

Did someone give a formal definition of normal and applicative order?

In all courses and textbooks I have seen, normal order reduction (NOR) and applicative order reduction (AOR) are defined as reducing respectively the leftmost outermost and rightmost innermost redex. ...
9
votes
2answers
449 views

Are a few hundred reduction steps too many to get the normal form of Y fac ⌜3⌝?

As I have been teaching the basis of λ-calculus lately, I have implemented a simple λ-calculus evaluator in Common Lisp. When I ask the normal form of Y fac 3 in ...
2
votes
2answers
157 views

how to formalize the class(?) of computational models and their equivalence

Introductory books to theoretical computer science usually introduce a the Turing machine and some of its variants, as well as the Random Access machine as computational models. Sometimes more ...
16
votes
1answer
681 views

Seeking Scott's original LCF paper

Is the following manuscript publically available? Dana Scott, 1969, A theory of computable functions of higher type. Unpublished seminar notes, 7 pages, University of Oxford. There is a discussion ...
5
votes
3answers
981 views

why is Linear Datalog interesting?

For those doesn't know about linear datalog, linear datalog is a datalog rule in which the number of IDB predicate in each rule is less or equal than one. My question is, why is this interesting? ...
7
votes
1answer
337 views

Implications of the rule of cumulativity in the Calculus of Constructions

Please help me understand some type theory research. As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or ...
12
votes
2answers
363 views

Modal logics axiomatised with nesting depth one which are unlikely to be in PSPACE?

I am looking for modal logics, which are axiomatised by a finite set of axioms of modal nesting depth one, and whose satisfiability / derivability problem is unlikely to be in PSPACE. Without the ...
12
votes
2answers
13k views

What is the difference between LTL and CTL?

I already read examples of formulas in CTL but not in LTL and vice-versa, but I'm having trouble gaining a mental grasp on LTL formulas and really what, at the heart, is the difference.
2
votes
2answers
253 views

Reversible Logic Circuit Synthesis [closed]

I am about to choose a project regarding "Reversible logic circuit synthesis". I've studied well about "Switching circuits and Logic design" and I found it very intriguing but I've got no idea about ...
9
votes
2answers
311 views

Does the order of declarations in an inductive type matter?

I was wondering if the order of declarations of an inductive type can matter. For example in Coq you can define Nat either by: ...
5
votes
1answer
325 views

A simple inference in rewriting theory

I was puzzled by a seeming simple inference in rewriting theory: if $y_1 \overset{*}{\leftarrow} x \overset{*}{\rightarrow} y_2$ then $y_1 \overset{*}{\leftrightarrow} y_2$. I don't understand how ...
24
votes
2answers
1k views

Do dependent types give you everything subtyping does?

Types and Programming Languages focuses quite a bit on subtyping, but as far as I can tell, subtyping doesn't seem especially fundamental. Does subtyping give you anything more than dependent types do?...
29
votes
1answer
902 views

Inductive types for large countable ordinal notations.

I'm looking to build notations for large countable ordinals in a "natural way". By "natural way" I mean that given an inductive data type X, that equality should be the usual recursive equality (the ...
8
votes
1answer
450 views

Can consume/produce be modeled in linear logic?

Question is whether it is possible to model in linear logic two modes of access to a resource. I know that two modes of resources are possible, i.e: $!r \vdash$ r is infinitely available $r \...
7
votes
1answer
163 views

Using MSOL for solving BIDS problem

From "Linear Time Solvable Optimization Problems on Graphs of Bounded Clique Width" (B. Courcelle et al) we know that any problem that can be written on MSOL (Monadic Second Order Logic) has a linear ...
6
votes
1answer
228 views

Papers on applying CTL over LTSs

Normally model checking with specifications written in CTL*/CTL is done over Kripke structures, however there are ways of doing it over somehow simpler Labelled Transition Systems, for instance ACTL. ...
46
votes
5answers
6k views

What is the most intuitive dependent type theory I could learn?

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
8
votes
2answers
522 views

What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?

I'm writing a toy modelchecker, and I'm at the point where it's time to implement LTL to Buchi automata translation. For a variety of obvious reasons, I wish the algorithm to be simple :) e.g. I want ...
11
votes
4answers
494 views

Finding a finite model

I know that the question "does a first order formula $\phi$ have a model" is undecidable in general. Could anyone give me a link or a book which give the answer for finite models. If I have a first ...
16
votes
3answers
1k views

What is the role of predicativity in inductive definitions in type theory?

We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A :...
6
votes
1answer
460 views

reference for lexicographic path ordering

Can you recommend a good reference for reading about lexicographic/recursive path orderings? I'm currently reading about lpo's in Chapter 2 of the Handbook of Automated Reasoning, 'Resolution Theorem ...
11
votes
2answers
339 views

References to programming languages based on conditional logics

Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; \square\!\!\!\!\...
37
votes
5answers
1k views

Results in Theoretical CS independent of ZFC

I'm going to ask a quite vague question, since the borderline between theoretical computer science and math is not always easy to distinguish. QUESTION: Are you aware of any interesting result in CS ...
15
votes
1answer
368 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 ...
15
votes
1answer
604 views

Fixed point theorems for constructive metric spaces?

Banach's fixed point theorem says that if we have a nonempty complete metric space $A$, then any uniformly contractive function $f : A \to A$ it has a unique fixed point $\mu(f)$. However, the proof ...

1
6 7
8
9 10