user: In this task, you are given a part of an article. Your task is to generate headline (title) for this text. Preferred headlines are under fifteen words.

Q: We define a logic of propositional formula schemata adding to the syntax of propositional logic indexed propositions (e.g., pi) and iterated connectives ∨ or ∧ ranging over intervals parameterized by arithmetic variables (e.g., ∧n i=1 pi, where n is a parameter). The satisfiability problem is shown to be undecidable for this new logic, but we introduce a very general class of schemata, called bound-linear, for which this problem becomes decidable. This result is obtained by reduction to a particular class of schemata called regular, for which we provide a sound and complete terminating proof procedure. This schemata calculus (called stab) allows one to capture proof patterns corresponding to a large class of problems specified in propositional logic. We also show that the satisfiability problem becomes again undecidable for slight extensions of this class, thus demonstrating that bound-linear schemata represent a good compromise between expressivity and decidability.

A: Decidability and Undecidability Results for Propositional Schemata
****
Q: Self-paced learning (SPL) has been attracting increasing attention in machine learning and computer vision. Albeit empirically substantiated to be effective, the investigation on its theoretical insight is still a blank. It is even unknown that what objective a general SPL regime converges to. To this issue, this study attempts to initially provide some new insights under this “heuristic” learning scheme. Specifically, we prove that the solving strategy on SPL exactly accords with a majorization minimization algorithm, a well known technique in optimization and machine learning, implemented on a latent objective. A more interesting finding is that, the loss function contained in this latent objective has a similar configuration with non-convex regularized penalty, an attractive topic in statistics and machine learning. In particular, we show that the previous hard and linear self-paced regularizers are equivalent to the capped norm and minimax concave plus penalties, respectively, both being widely investigated in statistics. Such connections between SPL and previous known researches enhance new insightful comprehension on SPL, like convergence and parameter setting rationality. The correctness of the proposed theory is substantiated by experimental results on synthetic and UCI data sets.

A: What Objective Does Self-paced Learning Indeed Optimize?
****
Q: In this paper we introduce RankPL, a modeling language that can be thought of as a qualitative variant of a probabilistic programming language with a semantics based on Spohn’s ranking theory. Broadly speaking, RankPL can be used to represent and reason about processes that exhibit uncertainty expressible by distinguishing “normal” from “surprising” events. RankPL allows (iterated) revision of rankings over alternative program states and supports various types of reasoning, including abduction and causal inference. We present the language, its denotational semantics, and a number of practical examples. We also discuss an implementation of RankPL that is available for download.

A:

assistant: RankPL: A Qualitative Probabilistic Programming Language
****