ABSTRACT. Automated inductive reasoning for term rewriting has been extensively studied in the literature. Classes of equations and term rewriting systems (TRSs) with decidable inductive validity have been identified and used to automatize the inductive reasoning. In this talk, a new approach for deciding inductive theorems of TRSs is described. In particular, we give procedures for deciding the inductive validity of equations in some standard TRSs on natural numbers and lists. Our essential idea is to use the validity in the initial algebras of TRSs, instead of validity guaranteed by existence of inductive proofs. Contrary to previous decidability results, our procedures can automatically decide without involving induction reasoning the inductive validity of arbitrary equations for these TRSs, that is, without imposing any syntactical restrictions on the form of equations.

• ISR 2014: Status Report
• ISR 2015: Progress Report
• ISR 2016: Proposals and Voting

ABSTRACT. We give a new proof of the decidability of reachability in alternating pushdown systems, showing that it is a simple consequence of a cut-elimination theorem for some logic.

ABSTRACT. SGGS, for Semantically-Guided Goal-Sensitive theorem proving, is a new inference system for first-order logic. It was inspired by the idea of generalizing to first-order logic the model-based style of the Davis-Putnam-Logemann-Loveland (DPLL) procedure for propositional logic. Model-based reasoning is a key feature of SAT solvers, SMT solvers, and model-constructing decision procedures for specific theories, and a crucial ingredient to their practical success. However, model-based reasoning in first-order logic is challenging, because the logic is only semi-decidable, the search space is infinite, and model representation is harder than in the propositional case. SGGS meets the challenge by realizing a seemingly rare combination of properties: it is model-based a la DPLL; semantically guided by an initial interpretation, to avoid blind guessing in an infinite search space; proof confluent, to avoid backtracking, which may be cumbersome for first-order problems; goal-sensitive, which is important when there are many axioms or a large knowledge base; and it uses unification to avoid enumeration of ground terms, which is inefficient, especially for rich signatures. In terms of operations, SGGS combines instance generation, resolution, and constraints, in a model-centric approach: it uses sequences of constrained clauses to represent models, instance generation to extend the model, resolution and other inferences to repair it. This talk advertises SGGS to the rewriting community, presenting the main ideas in the method: a main direction for future work is extension to first-order logic with equality, which requires rewrite-based reasoning. A manuscript including all aspects of SGGS, the technical details, the proofs of refutational completeness and goal-sensitivity, a comparison with other work (e.g., resolution with set of support, the disconnection calculus, the model evolution calculus, the Inst-Gen method) and more references, is available.

ABSTRACT. The Normalization Theorem (O'Donnell 1977) states that for every left-normal orthogonal rewrite system, the leftmost outermost strategy reduces any term to the normal form if it exists. Although the theorem ensures the normalization property of important systems like Combinatory Logic, the left-normality condition rules out many functional programs. We revisit the problem to seek a solution for normalization of the leftmost outermost strategy.

ABSTRACT. In traditional western music notation, the durations of notes are expressed hierarchically by recursive subdivisions. This led naturally to a tree representation of melodies widespread in systems for assistance to music authoring. We will see how term rewriting techniques can be applied to computer music problems, in particular to the problem of rhythm quantization: the transcription of a sequence of dates (real time values) into a music score. Besides the question of rhythm representation, an interesting problem in this context is the design and concise description of large rewrite rule sets and decision problems for these descriptions.