Rewrite method for theorem proving in first order theory with equalityJIEH HSIANG.Journal of symbolic computation. 1987, Vol 3, Num 1-2, pp 133-151, issn 0747-7171Article

A THEOREM-PROVING LANGUAGE FOR EXPERIMENTATION.HENSCHEN L; OVERBEEK R; WOS L et al.1974; COMMUNIC. A.C.M.; U.S.A.; DA. 1974; VOL. 17; NO 6; PP. 308-314; BIBL. 6 REF.Article

Z-module reasoning: an equality-oriented proving method with built-in ring axiomsWANG, T.-C.Journal of the Association for Computing Machinery. 1993, Vol 40, Num 3, pp 558-606, issn 0004-5411Article

Superposition with equivalence reasoning and delayed clause normal form transformationGANZINGER, Harald; STUBER, Jürgen.Information and computation (Print). 2005, Vol 199, Num 1-2, pp 3-23, issn 0890-5401, 21 p.Conference Paper

DATA STRUCTURES AND CONTROL ARCHITECTURE FOR IMPLEMENTATION OF THEOREM-PROVING PROGRAMSOVERBEEK RA; LUSK EL.1980; LECTURE NOTES COMPUTER SCI.; DEU; DA. 1980; VOL. 87; PP. 232-249; BIBL. 12 REF.Conference Paper

ADDING DYNAMIC PARAMODULATION TO REWRITE ALGORITHMSGLOESS PY; LAURENT JPH.1980; LECTURE NOTES COMPUTER SCI.; DEU; DA. 1980; VOL. 87; PP. 195-207; BIBL. 9 REF.Conference Paper

Paramodulation with Non-Monotonic Orderings and SimplificationBOFILL, Miquel; RUBIO, Albert.Journal of automated reasoning. 2013, Vol 50, Num 1, pp 51-98, issn 0168-7433, 48 p.Article

Well-foundedness is sufficient for completeness of ordered paramodulationBOFILL, Miquel; RUBIO, Albert.Lecture notes in computer science. 2002, pp 456-470, issn 0302-9743, isbn 3-540-43931-5, 15 p.Conference Paper

The shortest single axioms for groups of exponent 4KUNEN, K.Computers & mathematics with applications (1987). 1995, Vol 29, Num 2, pp 1-12, issn 0898-1221Article

Preuve automatique par paramodulation, réécriture et induction = Automatic proof by paramodulation, rewriting and inductionBouhoula, Adel.1992, 50 p.Report

An improved general E-unification methodDOUGHERTY, D. J; JOHANN, P.Journal of symbolic computation. 1992, Vol 14, Num 4, pp 303-320, issn 0747-7171Article

Automated deduction with associative comutative operators = Déduction automatique avec des opérateurs associatifs et commutatifsRussinowitch, Michaël; Vigneron, Laurent.1993, 36 p.Report

Rewrite-based deduction and symbolic constraintsNIEUWENHUIS, R.Lecture notes in computer science. 1999, pp 302-313, issn 0302-9743, isbn 3-540-66222-7Conference Paper

Déduction automatique avec contraintes symboliques dans les théories équationnelles = Automated deduction with symbolic constraints in equational theoriesVigneron, Laurent; Rusinowitch, M.1994, 178 p.Thesis

Automatic decidability and combinabilityLYNCH, Christopher; RANISE, Silvio; RINGEISSEN, Christophe et al.Information and computation (Print). 2011, Vol 209, Num 7, pp 1026-1047, issn 0890-5401, 22 p.Article