Tagged Questions

Computational and mathematical logic.

learn more… | top users | synonyms (2)

2
votes
0answers
66 views

Presburger Arithmetic Decision Procedures

What are good textbook references for Presburger Arithmetic decision procedures?
5
votes
1answer
119 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
37 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 ...
12
votes
2answers
381 views

Fixed points in computability and logic

This question has also been posted on Math.SE, http://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 ...
4
votes
1answer
108 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 ...
0
votes
0answers
33 views

Does the Y Combinator Contradict the Haskell-Howard Correspondence? [migrated]

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Haskell-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
13
votes
1answer
238 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
84 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 ...
23
votes
5answers
941 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 ...
4
votes
0answers
182 views

Balanced Boolean function satisfiability

Consider the following problem: Input: A Boolean black-box $U$ of a balanced Boolean function (balanced meaning equal number of satisfying and unsatisfying truth assignments) Output: A ...
-1
votes
1answer
81 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
159 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
90 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
255 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 ...
0
votes
1answer
116 views

Which formalism is best suited for automated theorem proving in set theory?

Abbreviations - FOL is first-order logic; NBG is Von Neumann–Bernays–Gödel set theory; SEP is Stanford Encyclopedia of Philosophy; HOL is higher-order logic; ATP is automated theorem proving. Context ...
1
vote
0answers
61 views

About the position of side conditions in an inference rule

Sometimes I see people put side conditions above the inference line as if they were premises of an inference rule. This feels strange. My understanding (which may be wrong) is that a side condition ...
6
votes
3answers
189 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
0answers
63 views

Hypersequents: proof term assigments or translations to hybrid logic

I've been looking at a modal logic with the axiom $$ (\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B)) $$ Roughly, this says that the ...
5
votes
1answer
93 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 ...
4
votes
1answer
123 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. ...
7
votes
2answers
295 views

What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

I am in possession of a book, which, inspired by Russell's Principia Mathematica (PM) and logical positivism, attempts to formalize a specific domain by determining axioms and deducing theorems from ...
1
vote
0answers
54 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 ...
2
votes
1answer
54 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 ...
4
votes
1answer
231 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 ...
2
votes
0answers
66 views

How to translate general recursion into a set of $\mu$-recursive operator applications?

I'm trying to find a scheme to translate a functional language with let rec into a set of primitives called "generalized arrows", i.e. $\kappa$-calculus with ...
5
votes
1answer
134 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 ...
3
votes
0answers
63 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 ...
1
vote
1answer
101 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}$. ...
3
votes
1answer
112 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 ...
2
votes
1answer
137 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
73 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 ...
4
votes
1answer
141 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" ...
5
votes
1answer
133 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 ...
6
votes
1answer
386 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 ...
0
votes
0answers
186 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 ...
3
votes
1answer
264 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 ...
7
votes
1answer
119 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 ...
3
votes
2answers
181 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 ...
7
votes
1answer
104 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
vote
2answers
95 views

Good description of Calculus of Inductive Construction

I want to learn more about Calculus of Inductive Constructions. What can you recommend to read on this topic? All the materials which I found are either in French or too basic (the Coq'Art book). The ...
2
votes
2answers
72 views

How to use Prop from UTT in Agda

In Ulf Norell's thesis he mentions that Agda is based on Luo's UTT. However, I can't find a way to use Prop there. Is there any way to do so?
3
votes
2answers
101 views

Well-formedness condition for inductive types

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
11
votes
1answer
198 views

Can we distinguish strictly syntactic and semantic methods in programming language?

While discussion strong normalization proofs, this comment contrasts the "normal forms model" with "purely syntactic methods". This brings me back to a more basic question: can we still distinguish ...
15
votes
1answer
305 views

Natural theorems proven only “to high probability”?

There are plenty of situations where a randomized "proof" is much easier than a deterministic proof, the canonical example being polynomial identity testing. Question: Are there any natural ...
6
votes
1answer
124 views

Is infinitary logic a logic in the sense of Gurevich?

Gurevich provides an exact definition of what Logic capturing PTIME is. An abstract logic $L$ consists of a set of $L[\tau]$-sentences for each vocabulary $\tau$, and a mapping that maps a property ...
6
votes
4answers
191 views

Simplification of Presburger formulas in practice

I have formulas in Presburger arithmetic (with initial ∀, but I can apply quantifier elimination so they are quantifier-free) that are fairly complicated, yet, in many useful cases, are equivalent to ...
8
votes
3answers
237 views

Is the class of primitive recursion functionals equivalent to the class of functions which Foetus proves to terminate?

Foetus, if you have not heard of it, can be read up on here. It uses a system of 'call matrices' and 'call graphs' to find all 'recursion behaviors' of recursive calls in a function. To show that a ...
9
votes
3answers
436 views

What are natural examples of non-relativizable proofs?

As I understand it, a proof that P=NP or P≠NP would need to be non-relativizable (as in recursion theory oracles). Virtually all proofs seem to be relativizable, though. What are good examples of ...
0
votes
0answers
52 views

Bringing rigor into discussions. Do we have a crowd-sourced sytematic reasoning system?

I am looking for ways to crowd-source systematic reasoning behind common and uncommon convictions, beliefs, science principles, software or product design, political views, etc. Today, discussions on ...
6
votes
0answers
191 views

Generalized sequential machine synthesis subject to language equivalence/inclusion and reachability

A generalized sequential machine (GSM) is a generalization of a Mealy machine where on each transition one input symbol is read and 0 or more output symbols are written. As in a Mealy machine, we ...