Research report Series C (275-286)

Research report Series C (117-276)

Notice! Some reports in this list may not have complete on-line information. In this case, or in general, if you have any question, please contact to the contacting author of the report directly.

ID: C-286 (April, 2019)

On the Completeness and the Decidability of Strictly Monadic Second-Order Logic

Author

Kento Takagi and Ryo Kashima

Email

takagi.k.am (at) m.titech.ac.jp kashima (at) is.titech.ac.jp

Regarding monadic second-order logic, it is known that there are no deductive systems which are sound and complete w.r.t. standard semantics, although w.r.t. Henkin semantics, a standard second-order deductive system with full comprehension is sound and complete. We show that as for strictly monadic second-order logic (SMSOL), which is the fragment of monadic second-order logic in which all predicate constants are unary and there are no function symbols, the standard deductive system is sound and complete w.r.t. standard semantics. This result is achieved by showing that in the case of SMSOL, the truth value of any formula in a faithful identity-standard Henkin structure is preserved when the structure is “standardized”; that is, the predicate domain is expanded into the set of all unary relations. In addition, we obtain a simpler proof of the decidability of SMSOL.

---

ID: C-285 (March, 2019)

A Note on the Undecidability of Quantified Announcements

Author

Yuta Asami

Email

asami.y.ac (at) gmail.com

In “The Undecidability of Quantified Announcements” T. Ågotnes, H. van Ditmarsch, and T. French (2016), there is an error in the proof of the undecidability of group announcement logic (GAL). The purpose of this note is to correct this error. We show that when there are two or more agents in the language, the satisfiability problem is undecidable for GAL.

---

ID: C-284 (August, 2016)

Completeness of Second Order Propositional Intuitionistic Logics

Author

Ryo Kashima

Email

kashima (at) is.titech.ac.jp

Abstract

We give alternative proofs of the completeness of two second order propositional intuitionistic logics with respect to Kripke models. One is the logic having the full comprehension axiom, and the other has the constant domain axiom in addition. We also show that, for disjunction free fragment, the constant domain axiom is not needed for the completeness with respect to constant domain models. To show the completeness, we use ``sequent tree calculi''.

---

C-283 (February, 2016)

Title

Linguistic Regularities from Multiple Samples

Author

Aleksandr Drozd and Satoshi Matsuoka

Email

alex (at) smg.is.titech.ac.jp

We present a simple method for better retrieval of analogical relations from word embeddings by learning from the multiple related pairs of words. We provide performance evaluation of the proposed method in comparison with the state-of-the-art approaches based on vector offset.

---

ID: C-282 (March, 2015)

Intuitionistic fragment of the lambda mu calculus

Author

Naosuke Matsuda

Email

matsuda. naosuke (at) gmail. com

Parigot gave an elegant proof system “the lambda mu calculus” for classical logic, and gave a correspondence between classical logic and some kind of program structures which the lambda calculus cannot capture. Although the correspondence is due to the power of inference rules of the lambda mu calculus, some of those rules are admissible in some intuitionistic proof systems. It therefore must be natural to ask whether it is possible to extend the correspondence between intuitionistic logic and program structures. In this paper, we give a partial answer to this question by giving a natural subsystem of the lambda mu calculus which corresponds to intuitionistic logic and investigating it.

---

ID: C-281 (November, 2014)

A PROOF THEORETIC STUDY ON INTUITIONISTIC TREE SEQUENT CALCULUS

Author

Naosuke Matsuda

Email

matsuda. naosuke (at) gmail. com

TLJ is a proof system for intuitionistic logic which has connections to many other areas of computer science and mathematics. In this paper, to make the base of those studies, we give a proof theoretic study on this system.

---

ID: C-280 (July, 2012)

The First Eigenvalue of $latex (c, d)$-Regular Graph

Author

Kotaro Nakagawa and Hiroki Yamaguchi

Email

watanabe(at)is. titech. ac. jp

We show a phase transition of the first eigenvalue of random $latex (c,d)$-regular graphs, whose instance of them consists of one vertex with degree c and the other vertices with degree $latex d$ for $latex c > d$. We investigate a reduction from the first eigenvalue analysis of a general $latex (c,d)$-regular graph to that of a tree, and prove that, for any fixed $latex c$ and $latex d$, and for a graph $latex G$ chosen from the set of all $latex (c,d)$-regular graphs with n vertices uniformly at random, the first eigenvalue of $latex G$ is approximately $latex \max(d, c/\sqrt{c-d+1})$ with high probability.

---

ID: C-279 (March, 2012)

Completeness of Hilbert-style axiomatization for the extended computation tree logic ECTL

Author

Ryo Kashima

Email

kashima(at)is.titech.ac.jp

We give a complete Hilbert-style axiomatization for ECTL, which is an extension of the Computation Tree Logic (CTL) with a modal operator ``infinitely often along some path’’.

---

A Projection-Based Method for Interactive Visual Exploration of Complex Graphs in A Three-Dimensional Space

ID

C-278 (February, 2012)

Author

Masanori Takami, Hiroshi Hosobe, Ken Wakita

Email

wakita(at)is. titech. ac. jp

Abstract

Complex networks can be hard for us human beings to conceptually grasp. We propose a new graph visualization method, which projects the static high-dimensional layout of a complex graph onto a two-, three-, or higher-dimensional space and allows viewers to explore the graph by interactively altering the way the layout is projected. The viewer could visually ``untangle’’ what initially appeared to be a tight knot — a simply impossible operation in conventional methods, with which you could just either zoom in or rotate. This is made possible by interpreting the user’s action as a rotation command of the original graph in its original space and then re-projecting it onto the target space. This work extends Hosobe’s previous work, whose target space could only be two dimensional, not three dimensional. The theoretical foundation of our technique and the lessons acquired from our early prototype are presented.

---

Applying DominoJ to GoF Design Patterns

ID

C-277 (December, 2011)

Author

YungYu Zhuang and Shigeru Chiba

Email

Zhuang(at)csg.is.titech.ac.jp

Abstract

In this report we study practical effectiveness of method slot, which is a new language construct integrating events and methods. We use its language implementation, DominoJ, to implement design patterns in the GoF book, and found that 16 out of 23 patterns can benefit from it. Here we list down the sample code in Java and DominoJ for the 16 patterns, and discuss the benefits.

---

Message Passing Algorithms for MLS-3LIN Problem

ID

C-276 (October, 2011)

Author

Osamu Watanabe

Email

watanabe(at)is. titech. ac. jp

Abstract

MLS-3LIN problem is a problem of finding a most likely solution for a given system of perturbed 3LIN-equations under a certain planted solution model. This problem is essentially the same as MAX-3XORSAT problem. We investigate the average-case performance of message passing algorithms for this problem, where input instances are generated under the planted solution model with equation probability p and perturbation probability q. For some variant of a typical message passing algorithm, we prove that p=Theta(1/(nln n)) is the threshold for the algorithm to work w.h.p.for any fixed constant q<1/2.

---

Fourier Approximation under Non-uniform Distribution

ID

C-275 (September, 2011)

Author

Hiroki Yamaguchi

Email

yamaguc6(at)is. titech. ac. jp

Abstract

We propose a generalization of a PAC-learning algorithm known as the Low Degree Learning Algorithm for non-uniform distributions. We show that our algorithm works under a non-uniform distribution D if the smallest eigenvalue of the Fourier coefficient matrix of the distribution is not too small. We also show that this condition is guaranteed if there are few examples which appear with very small probability under the distribution D.

Recent Posts