Questions tagged [lo.logic]

Computational and mathematical logic.

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 ...
Eric Anderson's user avatar
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)...
user1952009's user avatar
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 ...
John Wentworth's user avatar
1 vote
2 answers
120 views

Determine if a structure is a model of an inductively defined predicate

My setting is first-order logic. As an example, consider an inductive definition of a linked list: $List(l)$ = $Null(l)$ $\vee~(Node(l) \wedge \exists sublist. List(sublist) \wedge next(l,...
sean's user avatar
  • 722
1 vote
0 answers
188 views

Definitions of strongest postconditions [closed]

The weakest precondition of while loop $\mathtt{while}(G)\{C\}$ with respect to postcondition $P$ can be characterized by the least fixed point of the predicate transformer $X ~\mapsto \neg G \wedge ...
blk's user avatar
  • 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} $ ...
D. Rusin's user avatar
  • 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 ...
user1868607's user avatar
  • 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? ...
Petr's user avatar
  • 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 ...
StefanH's user avatar
  • 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 ...
Maja Piechotka's user avatar
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 ...
Andrew Polonsky's user avatar
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 ...
Aaron Rotenberg's user avatar
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 ...
Neel Krishnaswami's user avatar
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: ...
Pierre T.'s user avatar
  • 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 ...
Andrew Bacon's user avatar
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 ...
user_1_1_1's user avatar
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$ ...
StefanH's user avatar
  • 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 (...
StefanH's user avatar
  • 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 ...
StudentType's user avatar
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. -...
Joshua Grochow's user avatar
11 votes
1 answer
910 views

Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

So I've been wondering if the Law of Excluded Middle (LEM) implies the so-called Axiom K in Martin-Löf's Intensional Type Theory. The Axiom K states that $$\Pi_{A : Type} \Pi_{x : A} \Pi_{p : \text{Id}...
StudentType's user avatar
4 votes
0 answers
117 views

Transferring results on coalgebras in one category to another

Let $F$ and $G$ be endofunctors over categories $C$ and $ D$, respectively. Suppose that there is a forgetful functor $C \to D$ that has a left adjoint. Can we infer properties of $F$-coalgebras ...
Pteromys's user avatar
  • 895
11 votes
1 answer
286 views

Entscheidungsproblem vs. Unvollständigkeitssatz (soft question)

The first term is used by Hilbert in his 1928 work, but in Gödel's later work, the same thing is referred to as Unvollständigkeitssatz ("incompleteness theorem"). For today's German CS researchers, it ...
Frank's user avatar
  • 213
6 votes
2 answers
352 views

Is there an algorithm which gets incrementally "smarter" as it runs?

Mind the following program: n = 0 best = 0 while (true): if (hash(n) > best): best = hash(n) ++n If you leave this program running for 10 years, when ...
MaiaVictor's user avatar
  • 3,137
14 votes
0 answers
303 views

Categorical semantics for S5 modal logic?

Does anyone know where I can look to find out what the generally categorical semantics of S5 is? For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving ...
Neel Krishnaswami's user avatar
7 votes
1 answer
176 views

Intuitionistic fragments of classical logic

For what conditions on P and Q, does P ⊢ Q in classical logic imply ...
fread2281's user avatar
  • 255
8 votes
1 answer
148 views

About the origin of the names "immune" and "simple"

I have been wondering for a while about the origin of the names "immune" and "simple". I also posed the same question to Andrea Sorbi, who in turn involved a few more colleagues in the discussion. ...
Andrea Asperti's user avatar
2 votes
0 answers
58 views

Decidability of the monadic second-order theory of a class of finite structures

Let $L$ be the set of sentences in some logic. I am interested in cases where $L$ is the set of sentences in monadic second-order logic, or it is its $\Pi^1_1$ fragment. Let $K$ be a class of finite ...
Pteromys's user avatar
  • 895
2 votes
0 answers
121 views

Applications of the monoidal closed structure in LTL?

A simple model of temporal logic is via time-indexed truth functions. This lets us model the Boolean connectives, as well as the next-step operator and modal always operator: $$ \begin{array}{lclll} ...
Neel Krishnaswami's user avatar
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 ...
user833970's user avatar
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 ...
FNH's user avatar
  • 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 ...
Pteromys's user avatar
  • 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 ...
Juan Meleiro's user avatar
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 ...
TomR's user avatar
  • 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,...
Nicola Gigante's user avatar
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 ...
TomR's user avatar
  • 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 ...
John.C's user avatar
  • 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 ...
Marzio De Biasi's user avatar
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 ...
tci's user avatar
  • 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 ...
isekaijin's user avatar
  • 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 ...
Troy McClure's user avatar
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 ...
Troy McClure's user avatar
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-...
AnaK's user avatar
  • 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 ...
Nathan BeDell's user avatar
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 ...
valya's user avatar
  • 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?
S. Nabil's user avatar
  • 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(...
Boolean_functions's user avatar
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 ...
TomR's user avatar
  • 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-...
Boolean_functions's user avatar
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 ...
TomR's user avatar
  • 409

1 2 3
4
5
11