# Questions tagged [lo.logic]

Computational and mathematical logic.

548 questions
Filter by
Sorted by
Tagged with
1 vote
0 answers
83 views

### What logic(s) exist for attributing belief?

I'm looking for an appropriate formalism to represent "traceability" in claims, especially connecting conclusions to source materials in a rigorous way. For example, I'd like to be able to represent ...
2 votes
2 answers
430 views

### Automated proving that a program doesn't halt

If you are a computer and you are given a program $P$ (with no input parameter) that doesn't halt, how would you try proving it doesn't halt ? (here proving means convincing ourselves that it is true)...
• 145
10 votes
1 answer
267 views

### Equilibrium in a Halting Game

Consider the following 2-player game: Nature randomly picks a program Each player plays a number in [0, infinity] inclusive in response to nature's move Take the minimum of the players’ numbers, and ...
1 vote
2 answers
120 views

• 81
11 votes
2 answers
206 views

### Does the first order theory of a finite structure have bounded quantifier rank?

Let $\mathfrak{A}$ be any finite structure. Does its first order theory $\mathfrak{T} := \mathfrak{TH}(\mathfrak{A})$ have bounded quantifier rank, in the sense that there is a $q\in\mathbb{N}$ ...
• 207
5 votes
1 answer
175 views

### Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups

This is a follow-up question. In my previous question, I presented Welder proof assistant and I stated that I want to automate proofs about basic field theory. The only answer to this post states that ...
• 1,017
3 votes
2 answers
296 views

### Languages that lack contraction, weakening or exchange

When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange? ...
• 2,601
1 vote
0 answers
87 views

### Question on Turings Dissertation *Systems of Logic based on Ordinals*, Axiomatic Properties [closed]

I have a question on Alan Turing's Dissertation Systems of Logic Based on Ordinals, a scanned copy you can find here, or rewritten in LaTeX here, and also a copy of the published version here (but in ...
• 2,077
11 votes
1 answer
699 views

### What is the intuition behind linear logic?

I'm trying to understand linear logic to understand linear type systems better. However, when I read the rules, I fail to get an intuition behind it as I've done in modal logic - $\Box A$ means $A$ is ...
4 votes
0 answers
66 views

### Finite intersection property of polymorphic type families

Let $\Phi$ be a type functor definable in polymorphic lambda calculus: $$\alpha : * \vdash \Phi(\alpha) : *$$ $$f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$ Suppose further ...
3 votes
0 answers
152 views

### Efficiently computing the union of all minimal unsatisfiable constraint sets in a first-order unification problem

Suppose we are given a standard first-order unification problem, represented as a set $D$ of term equality constraints, such that the system $D$ as a whole is unsatisfiable. Consider the minimal ...
7 votes
0 answers
227 views

### Relationship between Pataraia's theorem and inductive-recursive definitions?

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
• 32.5k
3 votes
1 answer
474 views

### How to generate Skolem function in practice

Context: Skolemization is the process of removing the existential quantifiers in a first-order formula. The existential bounded variables are replaced with existential quantified function. Questions: ...
• 133
4 votes
0 answers
100 views

### Coherence spaces and full completeness for the implicative fragment of linear logic

Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$. I ...
• 453
1 vote
2 answers
73 views

### Algorithms to synthesize optimal plans satisfying temporal logic constraints

I know how NuSMV can be applied on a model to check if certain temporal logic statements are satisfied, particularly LTL. I also know of the LTL to BA conversion routines available online. I am ...
• 111
3 votes
2 answers
145 views

### Construct proof systems for common algorithmic task, like equivalence of regular expressions

A propositional proof system according to Cook and Reckhow for a language $L \subseteq \Sigma^{\ast}$ is a deterministic polynomial time function $f : \Sigma^{\ast} \to L$ that is onto. For $y \in L$ ...
• 2,077
5 votes
0 answers
163 views

### Salomaa's axiomatisation of regular languages and the use of regular expression in it

I am reading the classical article of A. Salomaa where he gives two axiom systems for regular sets and proofs consistency and completeness. As I have understood it, an axiomatic system in some logic (...
• 2,077
6 votes
1 answer
167 views

### How to mechanically derive the recursor of a type from its constructors?

In Martin-Löf Dependent Type Theory a type is commonly prescribed by how to construct its canonical terms and how to show that its canonical terms are definitionally equal. This means that the ...
• 777
18 votes
1 answer
993 views

### Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

Many theorems and "paradoxes" - Cantor's diagonalization, undecidability of hatling, undeciability of Kolmogorov complexity, Gödel Incompleteness, Chaitin Incompleteness, Russell's paradox, etc. -...
• 37.3k
11 votes
1 answer
910 views

• 32.5k
10 votes
1 answer
237 views

### Typo in the calculus of constructions paper?

In the classic the calculus of constructions paper there is a rule that states (page 7 of the pdf, page 101 of the original document) This rule would mean that any context is reducible to a member ...
• 546
16 votes
0 answers
224 views

### What is the background in algebraic geometry and representation theory needed for geometric complexity theory? [duplicate]

I'm a mathematics student in my junior year and I'm interested in computational complexity and specially geometric complexity theory. I'm going to learn algebraic geometry and representation theory ...
• 269
1 vote
0 answers
107 views

### Is there a signature of a first-order language that characterize the class of regular languages?

A previous question on this site was about extending the first-order logic with logical constants (quantifiers, fixed-point operators, etc.) to obtain a logical characterization of the class of ...
• 895
3 votes
0 answers
270 views

### Formal definition of Turing Completeness [closed]

Wikipedia states: In computability theory, a system of data-manipulation rules […] is said to be Turing complete or computationally universal if it can be used to simulate any single-taped Turing ...
4 votes
1 answer
133 views

### Sequent calculus for nonmonotonic/defeasible logics?

Is it possible to construct sequent calculus for nonmonotonic/defeasible logic? If it is possible then those logics can be encoded in proof assistants which require sequent calculus for logic to be ...
• 409
6 votes
0 answers
152 views

### Complexity of validity of first-order logic over finite words with bounded quantifier alternation?

I'm concerned with the validity problem for sentences of first-order logic over finite words, i.e. $FO[\le]$ interpreted over finite subsets of $\mathbb{N}$. AFAIK it should be nonelementary. However,...
• 1,588
2 votes
0 answers
180 views

### Connection between nonmonotonic logic and type theory (lambda calculus)

There is known connection between classical and modal logics and type theory (lambda calculus), but are there connections between nonmonotonic logics (e.g. defeasible logic) and type theory (lambda ...
• 409
3 votes
0 answers
134 views

### Evaluating boolean formula without knowing all values

I am looking for research approaches for the following problem: assume we have a set of $m$ computers, each carries a bit, and a Boolean formula $\varphi$ over those $m$ variables. The computers are ...
• 31
3 votes
2 answers
195 views

### Boundary between decidability and undecidability for small theories

There is a lot of research on the boundary between decidability and undecidability of the halting problem for small models of computation: Turing machines, tag systems, CAs, ... This boundary is ...
12 votes
1 answer
503 views

### Incomplete basis of combinators

This is inspired by this question. Let $\mathcal{C}$ be the collection of all combinators which only have two bound variables. Is $\mathcal{C}$ combinatorially complete? I believe the answer is ...
• 259
2 votes
1 answer
294 views

### Damas-Milner-like subset of the calculus of constructions with global type inference

Damas-Milner is a subset of System Fω that gives up expressivity (type-level computation) for usability (type inference). The experience with Haskell and ML attests to the practical value of this ...
• 501
1 vote
0 answers
140 views

### Consistency of MSOL over trees

I couldn't find any source speaking about the consistency of [Weak] Monadic Second Order Logic over Binary Trees (or over graphs with finite tree/clique width). I did find decidability results, and it ...
• 181
7 votes
0 answers
294 views

### MLTT vs. [weak] MSOL

I've noted that both Martin-Lof type theory and [Weak] Monadic Second-Order logic (eg over trees) enjoy the ability to express basically any finite computer program, in a decidable manner. I was ...
• 181
6 votes
1 answer
354 views

### Standard reference for basic model theory definitions

I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-...
• 203
11 votes
1 answer
538 views

### Is there a good notion of non-termination and halting proofs in type theory?

Constructive type theory with its basic interpretation under the curry howard correspondence consists only of total, computable functions. In the literature, some has been said on using "computational ...
17 votes
2 answers
1k views

### How to think about coherent spaces intuitively?

Linear Logic is interpreted using coherent spaces, and they feature prominently in Girard's papers. I know all the three main ways to formally define them, and they don't really pose any problem to ...
• 477
9 votes
1 answer
841 views

### What is the difference between unification and anti-unification?

I understand that in Unification we try to find a general solution to an equation between two terms, but what is anti-unification, and how is it different?
• 191
0 votes
1 answer
288 views

### In regards to the tautologies of a polynomially-bounded propositional proof system

In the book 'Logical Foundations of Proof Complexity', co-authored by Stephen Cook, the following definition is given: A proof-system $F$ is said to be polynomially-bounded if there is a polynomial p(...
1 vote
1 answer
97 views

### How to model degree variable in logic (new type of modal logic?)?

I am trying to model domain in logic (first order logic or some of modal logics) and I have variable which is degree and not true-false variable. There can be different conclusions depending on the ...
• 409
-1 votes
1 answer
125 views

### On the difference between propositional proof system and polynomially-bounded proof system

For the definition of a propositional proof system we have: An abstract proof system is a polynomial time function f whose range is equal to the set of tautologies. If τ is a tautology, then an f-...
1 vote
1 answer
147 views

### How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses

There are lot of applications of Horn clauses (notable examples include use of rules in cognitive architectures and knowledge bases, as well as use of rules in business rules programs). Are there ...
• 409