Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
22
votes
2answers
2k views

What was the original intent for the creation of Lambda calculus?

I've read that initially Church proposed the $\lambda$-calculus as part of his Postulates of Logic paper (which is a dense read). But Kleene proved his "system" inconsistent after which, Church ...
5
votes
2answers
2k views

Do past time LTL and future time LTL have the same expressiveness?

I would like to ask if anybody is aware of a paper comparing the expressiveness of past time LTL and that of (future time) LTL.
14
votes
1answer
467 views

Comparing the Kolmogorov complexity of theories

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(s) > L$ where $K(s)$ is the Kolmogorov complexity of string $s$ and $L$ is a sufficiently large ...
-4
votes
1answer
92 views

Temporal Logic - Until [closed]

I have a doubt, in Linear Temporal Logic LTL, does the Until operator require that the first occurrence is the first term of the formula? ex: a U b does require ...
11
votes
2answers
286 views

What is the complexity of the equivalence problem for read-once decision trees?

A read-once decision tree is defined as follows: $True$ and $False$ are read-once decision trees. If $A$ and $B$ are read-once decision trees and $x$ is a variable not occurring in $A$ and $B$, then $...
12
votes
1answer
508 views

Practical applications of parity games

Are there examples of practical applications of parity games, ie systems, in the real world, that can be represented as parity games ? Usually related documentation on parity games has almost never a ...
10
votes
1answer
278 views

Reference for the fact that (0=1) implies false requires a universe in MLTT

It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe. The proof is also fairly ...
5
votes
1answer
118 views

Logics for timed resource control

I'm studying proof theory and I've seen that linear logic can be used as a way to control resource usage, since by the propositions-as-types it is equivalent to the linear lambda calculus. Is there a ...
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)...
12
votes
3answers
615 views

Uses of $\infty$-categories in TCS

I'm not a theoretical computer scientist. I'm a stable homotopy theorist using $\infty$-categories. I've seen applications of category theory and topos theory to theoretical computer science, and I ...
5
votes
0answers
190 views

Are there any logics to formalize understanding?

Are there any logics (modal-based or others) to formalize the following statement: "agent A understands p". For example "agent A understands that Titanic sank because it hit an iceberg" Where "...
2
votes
2answers
159 views

Recommendations for References on undecidability of First Order Logic

I am currently reading Computability and Logic by Boolos Burgess Geoffrey for the proof on "undecidability of first order logic". however, I find the notations a bit confusing. Can anyone recommend ...
0
votes
2answers
226 views

Logic with Linear Programming

Can first-order logic be modeled/simulated as linear programming or integer programming? What about other forms of logic (say second order)? Update: am actually not a theory person, but more on the ...
26
votes
3answers
2k views

Translating SAT to HornSAT

Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about HornSAT seems to imply that it is, but I have not been able to chase down ...
15
votes
2answers
848 views

Fixed points in computability and logic

This question has also been posted on Math.SE, https://math.stackexchange.com/questions/1002540/fixed-points-in-computability-nd-logic I hope it is ok to also post it here. If not, or if it is too ...
11
votes
1answer
644 views

Simply typed lambda calculus and higher order logic

What is the relation between simply typed lambda calculus and higher order logic? Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related ...
1
vote
0answers
53 views

what is the meaning of “indicate substitution by priming metavariables”

This is a question about the usage of "indicate substitution by priming metavariables". For example, in the separation logic(it is not important whether familiar to this logic), I can understand the ...
4
votes
1answer
224 views

What is a term of the type $\bot\rightarrow A$?

The sentence $\bot\rightarrow A$ is provable in intuitionistic logic for any type $A$. The proof is trivial: \begin{align} \bot&\vdash\bot \\ \hline \bot&\vdash A \\ \hline &\vdash\bot\...
7
votes
2answers
1k views

Automated theorem proving via unsupervised approaches

This question Where and how did computers help prove a theorem? considers some automated theorem proving successes. However they seem to be mostly supervised approaches, such as with the 4 color graph ...
25
votes
5answers
2k views

Are there any annotated formal verification systems for pure functional programming languages?

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
19
votes
1answer
837 views

Scott's stochastic lambda calculi

Recently, Dana Scott proposed stochastic lambda calculus, an attempt to introduce probabilistic elements into (untyped) lambda calculus based on a semantics called graph model. You can find his ...
9
votes
1answer
362 views

First order satisfiability that doesn't have finite models

We know from Church's theorem that determining first order satisfiability is undecidable in general, but there are several techniques we can use to determine first order satisfiability. The most ...
-1
votes
1answer
110 views

Consistency and completeness of any arbitrary 3-valued logic? [closed]

Based on the explanations here [1] I know that 3-valued first order logic has many different versions, which differ in the definition of their operations (e.g. implication). All of these (as far as I ...
2
votes
1answer
409 views

Three-valued logic solver?

This is not my area, so apologizes if I am asking nonsense! I know that there are very good solver/theorem provers for solving 1st order logic. Now I have a problem, using 3-valued logic, but I am ...
3
votes
1answer
195 views

Decidability of first-order theory of real closed fields with functions

By a famous theorem of Tarski, the first-order theory of real closed fields is decidable, as it admits quantifier elimination. Can this result be extended so that propositions can be quantified over ...
2
votes
0answers
375 views

Theorem prover fails to find simple set theory proof?

I am trying to use an automated theorem prover (SNARK) to prove a theorem in first-order logic. Tarski claims in his "a work on mereology" that the goal is provable from assertions 1-3 but he does ...
19
votes
1answer
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?
6
votes
3answers
236 views

Solving problems by deciding a logic

I am curious to know when open problems have been solved by expressing them in a specific logic, and then showing that this logic is decidable. I have two distinct cases in mind: The problem is ...
6
votes
1answer
130 views

A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available ...
5
votes
1answer
182 views

Expressiveness of Infinitary Logic

I'm trying to put together a general picture of the expressiveness of some logics: First-Order Logics, Fixed-Point Logics, (Finite Variable) Infinitary Logics and the respected versions with Counting. ...
2
votes
1answer
71 views

Infinitary Counting Logics: 1-sorted vs. 2-sorted framework

There are two ways to extend infinitary logic with counting: Grädel's way (cf. p. 11): We extend $L_{\infty\omega}$ by introducing a counting existential quantifier: $$ \mathcal{A} \models \exists^{...
1
vote
0answers
111 views

(co-)Horn formulation of Frankl's union-closed sets conjecture

Based on comments on MO there is simple forumlation of Frankl's union-closed sets conjecture in terms of (co-)Horn. In co-Horn CNF at most one literal is negated in every clause (Horn CNF where every ...
6
votes
1answer
3k views

Does there exist a sentence of first-order logic that is satisfiable only in infinite models that do not have a finite algorithmic representation?

There exist sentences of first-order logic that are satisfiable and are satisfiable only by models of infinite size. However, all such sentences I can think of are satisfied by infinite models that ...
6
votes
1answer
342 views

Can factorial be encoded in the Kappa-calculus with fixed point operator?

Suppose we have a $\kappa$-calculus with operator $fix$, that could be used to transform function with type $(1 \rightarrow a) \rightarrow a$ to a value of type $1 \rightarrow a$. We use a normal ...
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. ...
3
votes
0answers
97 views

How to develop an effective notation for a partially ordered logic?

I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes: In intuitionistic ...
4
votes
1answer
428 views

Rules about Prop and Set in UTT

In Luo's UTT (type theory which is used in Agda, Idris, and other dependently typed programming languages), there're are two rules for $\Pi$ types. One for $\mathsf{Prop}$ and one for $\mathsf{Set}$. ...
5
votes
1answer
576 views

Types which correspond to sets of cardinality of continuum

Are types which correspond to sets with cardinality of continuum possible in MLTT (or in any other constructive theory)? On the first sight, they aren't, since elements of types are terms and we ...
11
votes
1answer
2k views

W-types vs Inductive types

Martin-Löf type theory uses W-types to define inductive structures like integers, lists, etc. However, calculus of inductive constructions doesn't use them in the same way, inductive types there seems ...
3
votes
1answer
1k views

Monomorphic vs Polymorphic type theory

I am currently reading the book Programming in Martin-Löf type theory by Nordström et al. In the book they have two important parts, one about monomorphic set theory and the other about polymorphic ...
1
vote
1answer
88 views

Do algorithms for solving parity games ignore other possible strategies for player V after finding one?

Solving parity games (from a "start" node) relies on the existence of a history-free winning strategy for player 0 (V) or 1 (R). Whether there is more than one such strategy is probably never ...
2
votes
0answers
344 views

Conversion technique/tool from temporal logic CTL,CTL* or LTL to μ-calculus

Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...
0
votes
0answers
330 views

Equational Logic and First Order Predicate Logic

I am interested in using Equational Theories (ET) together with Equational Logic (EL) found in algebraic specification languages such as CafeOBJ . I wish to use ET+EL to represent and prove sentences ...
5
votes
1answer
257 views

What does consistency mean for “computational theories” corresponding to inductive types?

I am currently reading the book by Luo on computation and reasoning. In the book he contrasts inductive types considered as computational theories with axiomatic theories widespread in "standard" ...
10
votes
1answer
1k views

Homotopy type theory and Gödel's incompleteness theorems

Kurt Gödel's incompleteness theorems establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic". Homotopy Type Theory provides an alternative ...
8
votes
1answer
193 views

Decidability of inductive invariant existence in Presburger arithmetic

Problem: Consider a finite number of control states (including an "initial" and a "bad" state), a finite number of integer variables, and for each ordered pair of states a transition relation ...
2
votes
1answer
342 views

What is logic programming and does it really add anything new to the logic?

I am acquinted with the basics of such notions as logic programming, monotonic and non-monotonic reasoning, modal logic (especially dynamic logic) and now I am wondering - does logic programming ...
6
votes
2answers
467 views

“Correctness” of type theory

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one? When type ...
8
votes
2answers
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 ...
9
votes
1answer
280 views

Example of where violation of strict positivity condition in inductive types leads to inconsistency

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?

1
3 4
5
6 7
10