Computational and mathematical logic.

learn more… | top users | synonyms (2)

4
votes
1answer
114 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" ...
4
votes
0answers
29 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 ...
5
votes
1answer
252 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
116 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
200 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
0answers
65 views

Possibility of refuting Steady State Universe theory? [closed]

The Steady-State universe theory was proposed in 1948 as an alternative to the notorious 'Big Bang theory'. While both assume an expanding universe in agreement with Einstein's predictions, the former ...
7
votes
1answer
100 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 ...
0
votes
0answers
145 views

Constructive proof for $(\forall x\in\mathbb N,P(x))\vee(\neg\forall x\in\mathbb N,P(x))$ given $(\forall x\in\mathbb N,P(x)\vee\neg P(x))$ [migrated]

I am trying to obtain the proof of the proposition: $(\forall x \in \mathbb{N}, P(x)) \vee (\neg \forall x, P(x))$ given that the property $P$ is decidable for every $x \in \mathbb{N}$, i.e. ...
3
votes
2answers
133 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
79 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
79 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
57 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
89 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. ...
8
votes
1answer
142 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
292 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
108 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
131 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 ...
7
votes
3answers
191 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
407 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
51 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
160 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 ...
0
votes
0answers
75 views

Given a CSL formula, how can we generate an automaton that accepts the formula?

The problem is same as the title, given a Continous Stochastic Logic(CSL) formula how can we create a machine which accepts the formula? Any intuitive ideas or references will be appreciated.
3
votes
1answer
197 views

Distributive expansion of CNF and implicants

I am looking for references for the following theorems. Theorem 1: Distributive expansion of a CNF formula $P_c$ (product of sums) results in a DNF formula (sum of products) consisting of all prime ...
6
votes
2answers
218 views

SAT in some DTIME always via a constructive proof?

Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are ...
1
vote
2answers
117 views

Why does IFP< not capture PTIME?

Consider the logic whose $\tau$-sentences are the sentences in $IFP(\tau \cup \{<\})$, and the satisfaction relation is given by $\mathfrak{A} \models^* \phi$ if $(\mathfrak{A}, <) \models ...
0
votes
0answers
153 views

Significance of Logic in Computer Science

I understand the significance of the theory of comptuation, for example NP-hardness of a problem signals us to forget about implementing it's exact solution and rather try approximating it. In the ...
1
vote
0answers
69 views

Conversion technique/tool from temoral 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 ...
8
votes
1answer
268 views

Hyperdoctrines and Monadic Second Order Logic

This question is essentially the question I asked on Mathoverflow. Monadic Second Order (MSO) logic is second order logic with quantification over unary predicates. That is, quantification over sets. ...
3
votes
2answers
231 views

Symbolic Execution is a case of Abstract Interpretation?

This is written in the wiki entry of Symbolic Execution, but I can't find any reference for it. Can anyone show me a pointer? Thank you.
2
votes
2answers
308 views

Questions about special types of partial assignments

Considering the definition "2-SAT: Given a CNF formula whose clauses have exactly 2 literals, does there exist an assignment of $\mathsf{TRUE}$ or $\mathsf{FALSE}$ to the variables that will ...
3
votes
2answers
141 views

Derivation of cut rule in sequent calculus

I searched internet but could not find any good weblink which shows how the cut rule for sequent calculus can be derived. I found this paper but it uses implication elimination rule which I cannot ...
3
votes
1answer
94 views

Program transformation using partial functions which preserve partial correctness

Much work has been done demonstrating that certain program transformations preserve particular properties. That is, for any program $P$ which has property $\alpha$, show that $P$ transformed under ...
1
vote
2answers
178 views

Using partial functions to prove correctness

I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates. Given: $P$ is a family of programs, parameterized by a function $f$. Write ...
12
votes
4answers
560 views

Start learning proof complexity

I recently started to read a lot about proof complexity and have been really enjoying what I have been reading. I would really like to learn more about this, but I am having difficulty finding some ...
5
votes
1answer
172 views

Lower bounds for formulae sizes for addition

I am interested in the conversion of $\sum_{i=1}^n x_i = y$ to 3-CNF. Here $x_i$ is a binary 0/1 variable and $y$ is some positive integer. There are a number of practical methods for doing this, ...
2
votes
2answers
168 views

All literals implied by a set of horn clauses

What is the name of this problem: given a set of Horn clauses (in fact just definite clauses and facts), find the set of literals which can be deduced from it. E.g. given $\{a, a \Rightarrow b, b ...
-3
votes
1answer
162 views

Discrepancy of solution in Logic in Computer Science book, please verify

I've come across a problem in the books exercises (exercise 1.4-17b), that asks of me to justify whether or not the $⊨ \phi$ holds for $((q \rightarrow (p ∨ (q \rightarrow p)) ∨ ¬(p \rightarrow q)) ...
5
votes
1answer
246 views

Bounded computation and incompleteness

Is there a complete theory T over a logical language L such that bounded computation may be encoded in it? Computational questions can be framed as arithmetical ones by interpreting them over natural ...
13
votes
1answer
202 views

Good reference about approximate methods for solving logic problems

It is known that many logic problems (e.g. satisfiability problems of several modal logics) are not decidable. There are also many undecidable problems in algorithm theory, e.g. in combinatorial ...
1
vote
1answer
215 views

Logic, language, semantics and more

I am working on a project that requires me to learn about logic (specially first order and second order). Looking for a good book or online reference that can help me with questions such as: A. What ...
2
votes
1answer
127 views

Typing relations terminology – how do I read typing relations?

I am currently trying to read up on type theory and have some quick questions on terminology. In the following rule, $$ \frac{x:T_1 \vdash t_2 : T_2}{\vdash \lambda x:T_1.t_2:T_1\to T_2} $$ How ...
1
vote
0answers
87 views

Satisfaction and synthesis of models in logics

It is well known that for propositional logic, the problem of constructing a model of a given formula is equivalent to deciding whether the formula has a model. Satisfiability is NP-complete, and ...
1
vote
1answer
172 views

What is resolution ((in FOL))? [closed]

I'm searching for an authoritative definition of resolution (logic resolution). Preferably on a reference freely available on the Internet (so I can read it right now). If this is too broad then ...
7
votes
1answer
160 views

Measurability of an $\omega$-regular language

It the previous question of mine I put a reference which shows that any $\omega$-regular language over the alphabet $\Sigma$ is a Borel subset of $\Sigma^\omega$. I am not sure whether the reference I ...
9
votes
1answer
531 views

Enumerate all solutions of a SAT problem

All the #SAT solvers I know, e.g RelSat, C2D, only return the number of satisfiable instances. But I want to know each of those instances? Is there such a #SAT solver or how I should modify an ...
3
votes
0answers
91 views

When can an inner existential quantifier be eliminated in favour of a function relating terms?

I have a question which somehow relates to the great answer by Bauer in the question Techniques for Reversing the Order of Quantifiers, where he discusses how the possibility of quantifier reversing ...
7
votes
4answers
199 views

What is the state of the art in theory of “Software transformations preserving behavior”?

I am interested in the field that could perhaps be referred to as "Automated Refactory" or "Preservation of Software Properties" after a transformation/change/refactory. Saying we have an ...
2
votes
1answer
75 views

What can we say about a fixed point for a provability predicate in deductively defined theory that satisfies diagonalisation lemma

I am wondering whether this is the right site to ask this question, but since it involves proof and diagonalisation, hopefully it is the right place. I am curious and trying to reason about what ...
15
votes
4answers
861 views

When does (or should) Theoretical CS care about intuitionistic proofs?

From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the ...
-1
votes
1answer
75 views

Constructing automata with the same traces, but where a CTL-formula is not equally satisfied [closed]

Hard to put this question in a short title. As part of a self-exercise, I'm trying to solve 6.15b of Principles of Model Checking by Baier and Katoen. You're supposed to prove that there does not ...