Cover Image

Instantiation theory : on the foundations of automated deduction /

Show other versions (1)

Instantiation Theory presents a new, general unification algorithm that is of immediate use in building theorem provers and logic programming systems. Instantiation theory is the study of instantiation in an abstract context that is applicable to most commonly studied logical formalisms. The volume...

Full description

Bibliographic Details
Main Author:	Williams, James G.
Corporate Author:	SpringerLink (Online service)
Format:	eBook
Language:	English
Published:	Berlin ; New York : Springer-Verlag, ©1991.
Series:	Lecture notes in computer science ; 518. Lecture notes in computer science. Lecture notes in artificial intelligence.
Subjects:	Automatic theorem proving. complétude. déduction automatique. complexité calcul. algorithme unification. homomorphisme. théorie algébrique. formalisme. instanciation. Théorèmes > Démonstration automatique. Deductie. Kunstmatige intelligentie. Electronic books.
Online Access:	Connect to the full text of this electronic book

Similar Items

Higher order logic theorem proving and its applications : 7th international workshop, Valletta, Malta, September 19-22, 1994 : proceedings /
Published: (1994)

Automated theorem proving /
by: Bibel, W., 1938-
Published: (1987)

Gems of theoretical computer science /
by: Schöning, Uwe, 1955-
Published: (1998)

Theory reasoning in connection calculi /
by: Baumgartner, Peter, 1962-
Published: (1998)

Automated theorem proving : a logical basis /
by: Loveland, Donald W.
Published: (1978)

The automation of reasoning with incomplete information : from semantic foundations to efficient computation /
by: Schaub, Torsten
Published: (1997)

Automated deduction in classical and non-classical logics : selected papers /
Published: (2000)

6th Conference on Automated Deduction, New York, USA, June 7-9, 1982 /
Published: (1982)

Automated deduction in equational logic and cubic curves /
by: McCune, W. (William)
Published: (1996)

5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980 /
Published: (1980)

Automated technology for verification and analysis : third international symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005 : proceedings /
Published: (2005)

Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX '97, Pont-à-Mousson, France, May 13-16, 1997 : proceedings /
Published: (1997)

A computational logic handbook /
by: Boyer, Robert S.
Published: (1988)

Isabelle : a generic theorem prover /
by: Paulson, Lawrence C.
Published: (1994)

A computational logic /
by: Boyer, Robert S., et al.
Published: (1979)

Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005 : proceedings /
Published: (2005)

Instantiation theory : on the foundations of automated deduction /
by: Williams, James G.
Published: (1991)

Logic programming and automated reasoning : 5th International Conference, LPAR '94, Kiev, Ukraine, July 16-22, 1994 : proceedings /
Published: (1994)

Automated theorem proving in software engineering /
by: Schumann, Johann M., 1960-
Published: (2001)

Symbolic computation and automated reasoning : the CALCULEMUS-2000 Symposium /
Published: (2001)

Theorem proving in higher order logics : 18th international conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005 : proceedings /
Published: (2005)

Isabelle/HOL : a proof assistant for higher-order logic /
by: Nipkow, Tobias, 1958-
Published: (2002)

From logic design to logic programming : theorem proving techniques and P-functions /
by: Snyers, Dominique, 1959-
Published: (1987)

The resolution calculus /
by: Leitsch, Alexander, 1952-
Published: (1997)

A many-sorted calculus based on resolution and paramodulation /
by: Walther, Christoph
Published: (1987)

A proof theory for general unification /
by: Snyder, Wayne, 1955-
Published: (1991)

Proof theory in computer science : international seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001 : proceedings /
Published: (2001)

Types for proofs and programs : International Workshop TYPES '94, Båstad, Sweden, June 6 - 10, 1994 ; selected papers /
Published: (1995)

Symposium on Automatic Demonstration : held at Versilles/France, December 1968 /
Published: (1970)

Handbook of automated reasoning /
Published: (2001)

Journal of automated reasoning.

Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings /
Published: (1998)

Computational logic and proof theory : Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993 : proceedings /
Published: (1993)

9th International Conference on Automated Deduction : Argonne, Illinois, USA, May 23-26, 1988 : proceedings /
Published: (1988)

The efficiency of theorem proving strategies : a comparative and asymptotic analysis /
by: Plaisted, David A.
Published: (1999)

Compositionality, concurrency, and partial correctness : proof theories for networks of processes and their relationship /
by: Zwiers, J. (Job), 1956-
Published: (1989)

Verifying temporal properties of systems /
by: Bradfield, J. C.
Published: (1992)

Logic for programming and automated reasoning : 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999 : proceedings /
Published: (1999)

Symbolic logic and mechanical theorem proving
by: Chang, Chin-Liang, 1937-, et al.
Published: (1973)

Artificial intelligence, automated reasoning, and symbolic computation : joint international conferences, AISC 2002 and Calculemus 2002, Marseille, France, July 1-5, 2002 : proceedings /
Published: (2002)