Termination of {aa → bc, bb → ac, cc → ab}HOFBAUER, Dieter; WALDMANN, Johannes.Information processing letters. 2006, Vol 98, Num 4, pp 156-158, issn 0020-0190, 3 p.Article

The Homer systemCOLTON, Simon; HUCZYNSKA, Sophie.Lecture notes in computer science. 2003, pp 289-294, issn 0302-9743, isbn 3-540-40559-3, 6 p.Conference Paper

Completeness results of inequality proversBLEDSOE, W. W; KUNEN, K; SHOSTAK, R et al.Artificial intelligence. 1985, Vol 27, Num 3, pp 255-288, issn 0004-3702Article

Les modèles analogiques et le contrôle dans les systèmes à base de règles = Analogical models and the control in rule-based systemsPloux, Sabine; Fouet, Jean-Marc.1992, 155 p.Thesis

Focus windows: A new technique for proof presentationPIROI, Florina; BUCHBERGER, Bruno.Lecture notes in computer science. 2002, pp 337-341, issn 0302-9743, isbn 3-540-43865-3, 5 p.Conference Paper

Strategic explanations for a diagnostic consultation systemHASLING, D. W; CLANCEY, W. J; RENNELS, G et al.International journal of man-machine studies. 1984, Vol 20, Num 1, pp 3-19, issn 0020-7373Article

Using the TPTP language for writing derivations and finite interpretationsSUTCLIFFE, Geoff; SCHULZ, Stephan; CLAESSEN, Koen et al.Lecture notes in computer science. 2006, pp 67-81, issn 0302-9743, isbn 3-540-37187-7, 1Vol, 15 p.Conference Paper

CODE : A powerful prover for problems of condensed detachmentFUCHS, D; FUCHS, M.Lecture notes in computer science. 1997, pp 260-263, issn 0302-9743, isbn 3-540-63104-6Conference Paper

A comparative study of COQ and HOLZAMMIT, V.Lecture notes in computer science. 1997, pp 323-337, issn 0302-9743, isbn 3-540-63379-0Conference Paper

Automatic verification by abstract interpretationCOUSOT, Patrick.Lecture notes in computer science. 2003, pp 20-24, issn 0302-9743, isbn 3-540-00348-7, 5 p.Conference Paper

How to prove inductive theorems? QUODLIBET!AVENHAUS, Jürgen; KÜHLER, Ulrich; SCHMIDT-SAMOA, Tobias et al.Lecture notes in computer science. 2003, pp 328-333, issn 0302-9743, isbn 3-540-40559-3, 6 p.Conference Paper

Foundations of proof search strategies design in linear logicPerrier, G; Galmiche, D.1994, 13 p.Report

A linguistic contribution to GOTO-less programmingCLARK, R. L.Communications of the ACM. 1984, Vol 27, Num 4, pp 349-350, issn 0001-0782Article

Symbolic solution of a piano movers' problem with four parametersLU YANG; ZHENBING ZENG.Lecture notes in computer science. 2006, pp 59-69, issn 0302-9743, isbn 3-540-31332-X, 1Vol, 11 p.Conference Paper

Proof confluent tableau calculiHÄHNLE, R; BECKERT, B.Lecture notes in computer science. 1999, pp 34-35, issn 0302-9743, isbn 3-540-66086-0Conference Paper

Transformational verification of parameterized protocols using array formulasPETTOROSSI, Alberto; PROIETTI, Maurizio; SENNI, Valerio et al.Lecture notes in computer science. 2006, pp 23-43, issn 0302-9743, isbn 3-540-32654-5, 1Vol, 21 p.Conference Paper

Workshop : The role of automated deduction in mathematicsCOLTON, S; SORGE, V; MARTIN, U et al.Lecture notes in computer science. 2000, issn 0302-9743, isbn 3-540-67664-3, p. 517Conference Paper

Finite acyclic theories are unitaryTHATTE, S. R.Journal of symbolic computation. 1993, Vol 15, Num 2, pp 235-249, issn 0747-7171Article

An Automated Derivation of Frege's Sentential Calculus from Lukasiewicz's CNHORNER, Jack K.Artificial intelligence. International conferenceWorldComp'2011. 2011, pp 190-196, isbn 1-60132-183-X 1-60132-184-8 1-60132-185-6, 7 p.Conference Paper

Unification modulo ACUI plus homomorphisms/distributivityANANTHARAMAN, Siva; NARENDRAN, Paliath; RUSINOWITCH, Michael et al.Lecture notes in computer science. 2003, pp 442-457, issn 0302-9743, isbn 3-540-40559-3, 16 p.Conference Paper

The Boyer-Moore Theorem Prover and its interactive enhancementBOYER, R. S; KAUFMANN, M; MOORE, J. S et al.Computers & mathematics with applications (1987). 1995, Vol 29, Num 2, pp 27-62, issn 0898-1221Article

A mechanical proof of the Church-Rosser theoremSHANKAR, N.Journal of the Association for Computing Machinery. 1988, Vol 35, Num 3, pp 475-522, issn 0004-5411Article

An Automated Derivation of Church's P₂ Sentential Calculus from Łukasiewicz's CNHORNER, Jack K.Artificial intelligence. International conferenceWorldComp'2011. 2011, pp 179-185, isbn 1-60132-183-X 1-60132-184-8 1-60132-185-6, 7 p.Conference Paper

An Automated Derivation of Łukasiewicz's CN from Frege's Sentential CalculusHORNER, Jack K.Artificial intelligence. International conferenceWorldComp'2011. 2011, pp 217-221, isbn 1-60132-183-X 1-60132-184-8 1-60132-185-6, 5 p.Conference Paper

Deciding inductive validity of equationsGIESL, Jürgen; KAPUR, Deepak.Lecture notes in computer science. 2003, pp 17-31, issn 0302-9743, isbn 3-540-40559-3, 15 p.Conference Paper