• 重庆市再次降低一般工商业电价 促进实体经济发展 2019-04-22
  • 许巍黄贯中金庆晧领衔 摇滚天团High翻理想音乐节 2019-04-22
  • 人民日报:传统节日,从美食走向美感 2019-04-22
  • 纳米专项结硕果:技术创新撬动50亿资本 2019-04-22
  • 睡不着时数绵羊真的不靠谱?五招让你做个好梦 2019-04-21
  • 安徽贯彻十九大:振兴美丽乡村,造福乡里乡亲 2019-04-21
  • 【萍乡天气】最新萍乡今天天气,实时提供萍乡气温、空气质量、24小时天气预报、生活指数查询 2019-04-19
  • 古力娜扎穿小西装化身清纯学生妹 热情拥抱粉丝 2019-04-19
  • 中欧班列让开放之路越走越宽 2019-04-13
  • “电商定制”价廉未必物美 成为“低价劣质”代名词 2019-04-13
  • 菜鸟世界杯送出50吨包裹-热门标签-华商网数码 2019-04-12
  • 曾祖父、曾祖母、祖父、祖母、父亲、母亲、重孙。一家7人,如果两家联姻,两家共十四人,请问:“看着就想笑”你那15人是咋算出来的? 2019-04-12
  • 权威解读!养老保险基金 中央怎么调剂? 2019-04-10
  • 欢乐“粽”情过端午 尽情放“粽”嗨起来 2019-04-05
  • 南昌重拳整治酒驾毒驾 2019-04-04
  • [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.
  • 重庆市再次降低一般工商业电价 促进实体经济发展 2019-04-22
  • 许巍黄贯中金庆晧领衔 摇滚天团High翻理想音乐节 2019-04-22
  • 人民日报:传统节日,从美食走向美感 2019-04-22
  • 纳米专项结硕果:技术创新撬动50亿资本 2019-04-22
  • 睡不着时数绵羊真的不靠谱?五招让你做个好梦 2019-04-21
  • 安徽贯彻十九大:振兴美丽乡村,造福乡里乡亲 2019-04-21
  • 【萍乡天气】最新萍乡今天天气,实时提供萍乡气温、空气质量、24小时天气预报、生活指数查询 2019-04-19
  • 古力娜扎穿小西装化身清纯学生妹 热情拥抱粉丝 2019-04-19
  • 中欧班列让开放之路越走越宽 2019-04-13
  • “电商定制”价廉未必物美 成为“低价劣质”代名词 2019-04-13
  • 菜鸟世界杯送出50吨包裹-热门标签-华商网数码 2019-04-12
  • 曾祖父、曾祖母、祖父、祖母、父亲、母亲、重孙。一家7人,如果两家联姻,两家共十四人,请问:“看着就想笑”你那15人是咋算出来的? 2019-04-12
  • 权威解读!养老保险基金 中央怎么调剂? 2019-04-10
  • 欢乐“粽”情过端午 尽情放“粽”嗨起来 2019-04-05
  • 南昌重拳整治酒驾毒驾 2019-04-04
  • 皇家北京赛车pk10手机 福彩刮刮乐的购买技巧 足彩进球彩18130 排列五走势图2元网 北京赛车pk10怎么赔付 经营彩票网站 福彩3d试机号 雪缘园足球比分 体彩排列5走势图 双色球中奖分布图 11选五多乐彩走势图 广西11选5 新时时彩中奖号码 天津时时彩又什么漏洞 广东快中彩玩法 139彩票网