University of Illinois Urbana-Champaign

Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification

Meseguer, José; Skeirik, Stephen

Content Files
inductive-reasoning.pdf

Permalink

https://hdl.handle.net/2142/107774

Description

Title
Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
Author(s)
  • Meseguer, José
  • Skeirik, Stephen
Issue Date
2020-07-16
Keyword(s)
  • induction
  • order-sorted logic
  • equality predicates
  • variants
Date of Ingest
2020-07-16T20:24:49Z
Abstract
We present an inductive inference system for proving validity of formulas in the initial algebra T[E] of an order-sorted equational theory E with 17 inference rules, where only 6 of them require user interaction, while the remaining 11 can be automated as simplification rules and can be combined together as a limited, yet practical, automated inductive theorem prover. The 11 simplification rules are based on powerful equational reasoning techniques, including: equationally defined equality predicates, constructor variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting and recursive path orderings. For E the union of E0 and B, these techniques work modulo B, with B a combination of associativity and/or commutativity and/or identity axioms
Type of Resource
text
Genre of Resource
technical report
Language
en
Permalink
http://hdl.handle.net/2142/107774
Sponsor(s)/Grant Number(s)
Partially supported by NRL under contract N00173-17-1-G002.

Owning Collections

Research and Tech Reports - Computer Science PRIMARY