Session 15B

Chair: Dale Miller

• 16:30: Timm Lampert, Anderson Nakano. Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates.     See abstract ...
  ABSTRACT. Modern logic engines widely fail to decide axiom sets that are only satisfiable in an infinite domain. This paper specifies a method to decide an infinite number of infinity axiom sets by strong infinity axiom sets (superpostulates). Any formula that is derivable from satisfiable superpostulates is also satisfiable. Starting from known infinity axioms, a complete infinity axiom set for pure first-order logic with only one binary relation (FOL$_{R}$) is specified. Based on complete theories, rules are defined to generate a system of infinity superpostulates based on a complete infinity axiom set. We generated a database with 1040 infinity superpostulates by running our algorithm. The paper ends with a discussion of the possibility of extending the method of specifying infinity superpostulates for FOL$_{R}$.
• 17:00: Liron Cohen, Reuben Rowe. Integrating Induction and Coinduction via Closure Operators and Proof Cycles.     See abstract ...
  ABSTRACT. Coinductive reasoning about infinitary data structures has many applications in computer science. Nonetheless developing natural proof systems (especially ones amenable to automation) for reasoning about coinductive data remains a challenge. This paper presents a minimal, generic formal framework that uniformly captures applicable (i.e. finitary) forms of inductive and coinductive reasoning in an intuitive manner. The logic extends transitive closure logic, a general purpose logic for inductive reasoning based on the transitive closure operator, with a dual 'co-closure' operator that similarly captures applicable coinductive reasoning in a natural, effective manner. We develop a sound and complete non-well-founded proof system for the extended logic, whose cyclic subsystem provides the basis for an effective system for automated inductive and coinductive reasoning. To demonstrate the adequacy of the framework we show that it captures the canonical coinductive datatype: streams.