How Does Resolution Works in Propositional Calculus and Predicate Calculus, Introduction to Unification and Substitution
|
10.5120/17409-7983 |
Dipanjan Kumar Dey. Article: How Does Resolution Works in Propositional Calculus and Predicate Calculus, Introduction to Unification and Substitution. International Journal of Computer Applications 99(10):22-31, August 2014. Full text available. BibTeX
@article{key:article,
author = {Dipanjan Kumar Dey},
title = {Article: How Does Resolution Works in Propositional Calculus and Predicate Calculus, Introduction to Unification and Substitution},
journal = {International Journal of Computer Applications},
year = {2014},
volume = {99},
number = {10},
pages = {22-31},
month = {August},
note = {Full text available}
}
Abstract
One of the most important rules of interference is resolution. Resolution basically works by using the principle of proof by contradiction. Propositional Resolution works only on expressions in clausal form. Before the rules of resolution can be applied, the premises and conclusions must be converted to this form. First part of this work consists of basic information about resolution like what are literals, clauses, empty clause, predicate, facts, rules, conjunctive normal form etc. What is it used for, what is their aim. One of the aims of this work is differentiating resolution between clauses-when clauses containing variables and When clauses containing no variables. When clauses containing no variables resolution are very easy and simple and then no need to substitution. When clauses containing variables resolution becomes complicated and then need a proper substitution through the cancellation of complementary literals. So substitution is an important role in resolution. Unification has been used in my work for performing resolution in predicate calculus. The unification algorithm tries to find out the Most General Unifier (MGU) between a set of atomic formulae. Theorem proving using resolution has also been included in my work which helps to solve many problems.
References
- [Pastre2002] D. Pastre, Strong and weak points of the MUSCADET theorem prover, AI Communications, 15(2- 3):147-160, 2002, http://www. cs. miami. edu/_tptp.
- [Pastre1993] D. Pastre, Automated Theorem Proving in Mathematics, Annals on Artificial Intelligence and Mathematics,8(3-4):425–447, 1993.
- [Robinson1965] J. A. Robinson, A machine oriented logic based on the resolution principle, J. ACM12:23-41, 1965.
- [Bledsoe1977] W. W. Bledsoe, Non-Resolution Theorem Proving, Journal of Artificial Intelligence,9:1–35, 1977.
- Artificial Intelligence: A Modern Approach by Stuart Russell and Peter Norvig, Secong Edition, Published 2003 Prentice Hall .
- [Jec97] Jech, T. J. : Set Theory, 2nd edn. Perspectives in Mathematical Logic. Springer, Berlin (1997).
- Chang C and Lee R, Symbolic Logic Mechanical Theorem proving, Academic press, New York, 1973.
- Nilsson N Principal of Artificial Intelligence, Tioga Publishing Company, 1980.
- Winston P H Artificial Intelligence, 2nd edition, Addison-Wesley, Menlo-Park, California, 1984.
- Foundation of artificial intelligence and expert system by Janakiraman.
- Artificial intelligence,3rd edn, by Elaine Rich ,Kevin Knight, Shivashankar B Nair.
- Introduction to 'Artificial intelligence and expert system' by Dan W. Patterson, PHI
- Resolution By Ankit Shah, Professor Harper Langston Discrete Mathematics Summer 2007
- Artificial intelligence notes- reasoning methods, lecturer: Co?kun Sönmez