• 10月26日十九大新闻发言人专题新闻发布会 2018-12-14
  • 2015年河北省公益广告作品展 2018-12-13
  • [06-29] Conditional Congruence Closure Algorithms for Uninterpreted and Interpreted symbols

    文章来源:  |  发布时间:2018-06-28  |  【打印】 【关闭

      

    全程打闲一年100万 www.edria.net Title:  Conditional Congruence Closure Algorithms for Uninterpreted and Interpreted symbols

    Speaker:   Prof. Deepak Kapur, Distinguished professor of University of New Mexico, USA

    Time:  10:00 am, June 29th, 2018

    Venue:  Room 337, Building 5, State Key Laboratory of Computer Science,Institute of Software, Chinese Academy of Sciences
     
    Abstract:
    Algorithms for generating congruence closure of conditional and unconditional equations on ground terms with uninterpreted and interpreted symbols are presented. A framework for generating  conditional equivalence closure of constant equations and constant Horn equations is discussed building on Tarjan's Union Find algorithm. A rewrite framework for generating a canonical constant Horn rewrite rules is given. This framework is then extended to include non-constant function symbols. Uninterpreted terms are flattened using new constants whereas equalities over interpreted terms belonging to the same theory are analyzed. The framework is general and flexible and can be used to develop congruence closure algorithms for cases when function symbols satisfy properties such as commutatively, associativity and commutativity, and/or idempotency and identity.Since the crucial  property exploited in congruence closure algorithm by Downey, Sethi and Tarjan as well as by Kapur (RTA97) is non-constant terms having unique signatures, signature computations are extended to ensure this property for extensions to interpreted symbols.The complexity of the conditional congruence closure is shown to be $O(n*log(n))$, which is the same as for unconditional ground equations. The proposed algorithm is motivated by our attempts to generate efficient and succinct interpolants for the quantifier-free theory of equality over uninterpreted function symbols which are often a conjunction of conditional equations and needs additional simplification.
  • 10月26日十九大新闻发言人专题新闻发布会 2018-12-14
  • 2015年河北省公益广告作品展 2018-12-13