Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
8
votes
2answers
361 views

Original Hoare Logic termination paper

I'm looking for the original paper where Hoare (or someone else I suppose) discusses termination (Total Correctness). Or any other early work on termination for "vanilla" Hoare logic (I suppose by ...
11
votes
1answer
374 views

MSO properties, planar graphs and minor-free graphs

Courcelle's theorem states that every graph property definable in monadic second-order logic can be decided in linear time on graphs of bounded treewidth. This is one of the most well-known ...
26
votes
1answer
543 views

Interesting algorithms in the formalization of the Feit-Thompson theorem?

It looks like George Gonthier and his collaborators have finished formalizing the Odd Order Theorem. In his earlier work on the Four Color Theorem, Gonthier invented a bunch of new algorithms (...
2
votes
1answer
119 views

Formal Methods Applied to Role-Based Security (RBAC)

I wonder if someone could direct me to a basic introduction to formal methods applied to role-based security. I'm particularly interested in the question of formal verification and the kind of ...
15
votes
1answer
321 views

What can we prove with infinite graphs that we cannot prove without them?

This is a follow-up question to this one about infinite graphs. Answers and comments to that question list objects and situations which are naturally modeled by infinite graphs. But there are also ...
9
votes
2answers
247 views

Closure ordinals for inductive types with function spaces

Functors built from finite products and sums have closure ordinal $\omega$, detailed nicely in this manuscript by Francois Metayer. i.e. we can reach the inductive type $nat := \mu X. 1 + X$ by ...
14
votes
1answer
1k views

A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
-2
votes
1answer
250 views

Problem in embedding

I want to embed PPTL(a kind of logic) in Coq. Because of its complex semantics, I just embed its systax. ...
44
votes
2answers
6k views

Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
23
votes
1answer
534 views

Unification and Gaussian Elimination

Does anyone knows of references that precisely spell out the connection between the unification algorithm and Gaussian elimination? I'm particularly interested in the relationship between triangular ...
2
votes
0answers
342 views

Encoding a logic in Coq

I want to encode a logic into Coq. The semantics of the logic are very complex and I just want to encode the syntax, axioms, inference rules. I use deep embedding, but I can't use notation like: <...
48
votes
8answers
4k views

Are there non-constructive algorithm existence proofs?

I remember I might have encountered references to problems that have been proven to be solvable with a particular complexity, but with no known algorithm to actually reach this complexity. I struggle ...
19
votes
0answers
1k views

What's the expressive power of Simply Typed Lambda calculus?

The standard approach to simply typed lambda calculus considers computations over Church numerals. If input and outputs are Church numerals always typed as $Int$, where $Int = (\tau \rightarrow \tau) ...
4
votes
1answer
317 views

Exponential blowup in Simple Proof of a theorem of Statman by Mairson

I'm studying "A simple proof of a theorem of Statman" by H.G. Mairson. At page 4, he encodes set/type theory in lambda calculus. In particular, note che "op" trick in the definition of $eq_{k+1}$. ...
3
votes
1answer
155 views

Commutative operators in unification

Say I want to find a unification for the following two sentences in first-order logic: P(x) & Q(y) Q(A) & P(B) Common sense tells us that {x: B, y: A} is such a unification. However, if I ...
9
votes
1answer
344 views

FO-uniform AC0 with some predicate

My question is about finite model theory/descriptive complexity, so $FO(R)$ will mean "first order over finite binary words, using predicates Rs and a unary predicate P true on the position of the 1 ...
15
votes
1answer
444 views

How efficient are DPLL-based SAT-solvers on satisfiable instances of PHP?

We know that DPLL based SAT-solvers fail to answer correctly on unsatisfiable instances of $\mathrm{PHP}$ (pigeon hole principle), e.g. on "there is a injective mapping from $n+1$ to $n$": $$\mathrm{...
22
votes
2answers
835 views

Circuit lower bounds and kolmogorov complexity

Consider the following reasoning: Let $K(x)$ denote the Kolmogorov complexity of the string $x$. Chaitin's incompleteness theorem says that for any consistent and sufficiently strong formal ...
11
votes
1answer
448 views

Extensionality of lambda calculus models

I'm translating a book on LISP and naturally it touches some elements of $\lambda$-calculus. So, a notion of extensionality is mentioned there alongside some models of $\lambda$-calculus, namely: $\...
9
votes
1answer
331 views

Reading list on rewriting systems?

I am new to studying rewriting systems as a first year PhD student. I would like to propose a special topics course on rewriting theory, and I want to make sure I don't leave any of the original ...
3
votes
1answer
155 views

Explanation of definition of normalizing: 9.1.12 in Terese “Term Rewriting Systems”?

A strategy for a rewriting system is a sub-rewriting system with the same objects and same normal forms. Definition (from Terese "Term Rewriting Systems"). Let N be a superset of the normal forms of ...
-1
votes
2answers
1k views

Kripke model and LTL vs CTL formulae interpretation [closed]

I have this Kripke model $M$: $$ \begin{array}{ccccccc} \to & (p, q) & \to & (\neg p, \neg q) & \to & (p, \neg q) \\ & \circlearrowright & & & & \...
3
votes
0answers
121 views

Expansion normal forms of confluent term rewriting systems

Suppose one has two rewrite rules $\to^\eta,\to^\beta$, both of which are confluent and such that $\to^A := \to^{(\eta \cup \beta)}$ is also confluent. Define a $\beta$-normal form relative to $\eta$ ...
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 ...
12
votes
2answers
801 views

Expressiveness of Büchi vs CTL(*)

What is the relationship between the expressiveness of LTL, Büchi/QPTL, CTL and CTL*? Can you give some references that cover as many of these temporal logics as possible (especially between linear- ...
5
votes
2answers
628 views

Do Higher-Order Functions provide more power to Functional Programming?

My original question was: Is Kappa calculus less powerful than Lambda calculus? Does the lack of Higher-Order functions on a programming language excludes some programs that could only be written in ...
15
votes
4answers
612 views

Unary parametricity vs. binary parametricity

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( https://dl.acm.org/citation.cfm?id=2359499). In this paper, they internalize unary ...
6
votes
1answer
270 views

Forms of types in the calculus of constructions

In the usual presentations of the calculus of constructions (CC) with two kinds Prop and Type such that Prop:Type and impredicative on Prop, it is easy to show the following result: every closed term ...
0
votes
1answer
136 views

Logic programming with integer or even floating point domains

I am reading a lot about logic programming - ASP (Answer Set Programming) is one example or this. They (logic programs) are usually in the form: [Program 1] Rule1: a <- a1, a2, ..., not am, am+1; ...
10
votes
1answer
278 views

Unification-based elimination rule for equality

A few years back, I ran across the following left-rule for equality in sequent calculus: $$ \frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t ...
8
votes
4answers
223 views

Why valuations when defining FOL?

Why does one need valuations in order to define the semantics of first-order logic? Why not just define it for sentences and also define formula substitutions (in he expected way). That should be ...
8
votes
1answer
249 views

Origin of Church encodings

In which paper did Alonzo Church first describe Church encoding? I can't find any articles that actually cite the paper, but I am interested in reading it.
5
votes
1answer
226 views

Resolution vs Extended Resolution

Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a ...
-2
votes
1answer
554 views

Coq definition with unusual syntax (Definition … Defined.)

While examining the package Library ZFC.Sets, I found the following definition: ...
15
votes
3answers
1k views

Checking formulas with two quantifiers ($\forall \exists$) - 2QBF

SAT solvers give a powerful way to check the validity of a boolean formula with one quantifier. For instance, to check the validity of $\exists x . \varphi(x)$, we can use a SAT solver to determine ...
11
votes
3answers
2k views

How to prove that a formula can not be expressed in LTL, but can be in Buchi automata?

I am looking for a general technique which can help me to prove not just that Buchi automata is more expressive model than LTL, but that the specific formula can/can't be expressed in LTL. For ...
22
votes
2answers
3k views

What's the difference between ADTs, GADTs, and inductive types?

Might anyone be able to explain the difference between: Algebraic Datatypes (which I am fairly familiar with) Generalized Algebraic Datatypes (what makes them generalized?) Inductive Types (e.g. Coq) ...
2
votes
0answers
134 views

Expressive power of (versions of) weighted average

Consider the arithmetic expressions obtained by allowing the constants 0 and 1, boolean variables, and allowing the operations $\min\{s,t\},\max\{s,t\}$, and $1-t$ where $s,t$ are expressions. Clearly ...
14
votes
0answers
296 views

Proof assistant formalizations of Finite Model Theory

I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would ...
3
votes
2answers
183 views

Labels for terms in the lambda calculus

In the lambda calculus, are there commonly accepted names for $x$ and $M$ when they appear in $\lambda x [M]$ ? Something along the lines of "binder" and "bindee"?
16
votes
1answer
992 views

Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
15
votes
2answers
690 views

Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?

I've been searching for a formalization of the compactness theorem for FOL, but haven't found any. Is anyone aware of such a development or related work?
17
votes
3answers
644 views

What is the minimal extension of FO that captures the class of regular languages?

Context: relations between logic and automata Büchi's Theorem states that Monadic Second Order logic over strings (MSO) captures the class of regular languages. The proof actually shows that ...
3
votes
3answers
315 views

Automatic proofs or model checking in an extremely simplified functional language

Imagine a stripped down functional programming language, that has the following properties The only value type is an integer There are no side effects Functions are defined as a single expression, ...
9
votes
1answer
497 views

Functional Completeness of 3-valued logic

In the context of some recent work, we have been defining a language based on a three-valued logic à la Kleene, where $1$ stands for true, $0$ for false, and $\bot$ for error or don't-know. In order ...
28
votes
6answers
9k views

What is the difference between propositions and judgments?

I get confused by the subtle difference between propositions and judgments when exposed to intuitionistic type theory. Can any one explain to me what is the point to distinguish them and what ...
3
votes
2answers
353 views

Does using Normal Order Evaluation instead of Normal Order Reduction lose the Normalization theorem?

Normal Order Reduction (NOR) reduce the leftmost, outermost redex. Normal Order Evaluation (NOE) reduce the leftmost, outermost redex, but not within the body of abstractions. So (λw. (λx.x) z) is ...
4
votes
2answers
408 views

Minimize a datalog program

We can consider a datalog program as a set of clauses. Some of them allow to derive others. For instance from: A(x) :- B(x), C(x). B(x) :- D(x). C(x) :- D(x). We ...
7
votes
1answer
282 views

How to define eta-equivalence for F-omega types?

There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus: via a plain relation $t_1 = t_2$, via an indexed relation $\Gamma \vdash t_1 = t_2 : T$...
1
vote
1answer
336 views

Can “$x(\lambda y.P\;)z$” be $\beta$-reduced?

Consider the untyped $\lambda$-calculus expression $$x(\lambda y.P\;)z$$ ...where (FWIW) $z$ is not free in $P$, and $P$ does not contain a redex. Can this expression be $\beta$-reduced? I've ...

1
6
7
8 9 10