{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T15:07:22Z","timestamp":1748617642608},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Over the past decades, a number of calculi for automated<\/jats:p><jats:p>reasoning have been proposed that share some core features:<\/jats:p><jats:p>1. proofs are built in a tableau\/sequent style as trees where<\/jats:p><jats:p>nodes are labeled with literals, and 2. these proofs are expanded<\/jats:p><jats:p>by interpreting the problem clause set as a set of rules, and<\/jats:p><jats:p>requiring all negative literals in clauses to present on a branch<\/jats:p><jats:p>for expansion.  This applies to hyper-tableaux, MGTP, coherent<\/jats:p><jats:p>logic, and others.  Existing implementations typically spend much<\/jats:p><jats:p>of their time in the process of matching branch literals with the<\/jats:p><jats:p>negative literals of the input clauses.  We present an<\/jats:p><jats:p>alternative to this matching process by applying a modified<\/jats:p><jats:p>version of the RETE algorithm.  The RETE algorithm was developed<\/jats:p><jats:p>in the 1970s for production systems in artificial<\/jats:p><jats:p>intelligence. We exploit the similarities between the mentioned<\/jats:p><jats:p>calculi and production systems in order to make the RETE<\/jats:p><jats:p>algorithm solve the matching problem.  We also investigate the<\/jats:p><jats:p>effect of working on several independent branches present in<\/jats:p><jats:p>tableau proof search but not in production systems.<\/jats:p>","DOI":"10.29007\/r5m4","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:57:36Z","timestamp":1516730256000},"page":"4--11","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Rule-Matching for Hyper-Tableaux"],"prefix":"10.29007","volume":"22","author":[{"given":"Bjarne","family":"Holen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dag","family":"Hovland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Giese","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"IWIL 2012. The 9th International Workshop on the Implementation of Logics"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:58:36Z","timestamp":1516730316000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/SC7c"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/r5m4","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}