CFP last date
20 January 2025
Call for Paper
February Edition
IJCA solicits high quality original research papers for the upcoming February edition of the journal. The last date of research paper submission is 20 January 2025

Submit your paper
Know more
The week's pick
Responsive image
SFLA-Based Line Balancing and Task Optimization in Master-Slave Controlled Hanger Transportation Systems for Garment Production

Duc Hoang Nguyen
Random Articles
Reseach Article

How Does Resolution Works in Propositional Calculus and Predicate Calculus, Introduction to Unification and Substitution

by Dipanjan Kumar Dey
journal cover thumbnail

International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 99 - Number 10
Year of Publication: 2014
Authors: Dipanjan Kumar Dey
10.5120/17409-7983

Dipanjan Kumar Dey . How Does Resolution Works in Propositional Calculus and Predicate Calculus, Introduction to Unification and Substitution. International Journal of Computer Applications. 99, 10 ( August 2014), 22-31. DOI=10.5120/17409-7983

@article{ 10.5120/17409-7983,
author = { Dipanjan Kumar Dey },
title = { How Does Resolution Works in Propositional Calculus and Predicate Calculus, Introduction to Unification and Substitution },
journal = { International Journal of Computer Applications },
issue_date = { August 2014 },
volume = { 99 },
number = { 10 },
month = { August },
year = { 2014 },
issn = { 0975-8887 },
pages = { 22-31 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume99/number10/17409-7983/ },
doi = { 10.5120/17409-7983 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T22:27:51.024858+05:30
%A Dipanjan Kumar Dey
%T How Does Resolution Works in Propositional Calculus and Predicate Calculus, Introduction to Unification and Substitution
%J International Journal of Computer Applications
%@ 0975-8887
%V 99
%N 10
%P 22-31
%D 2014
%I Foundation of Computer Science (FCS), NY, USA
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
  1. [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.
  2. [Pastre1993] D. Pastre, Automated Theorem Proving in Mathematics, Annals on Artificial Intelligence and Mathematics,8(3-4):425–447, 1993.
  3. [Robinson1965] J. A. Robinson, A machine oriented logic based on the resolution principle, J. ACM12:23-41, 1965.
  4. [Bledsoe1977] W. W. Bledsoe, Non-Resolution Theorem Proving, Journal of Artificial Intelligence,9:1–35, 1977.
  5. Artificial Intelligence: A Modern Approach by Stuart Russell and Peter Norvig, Secong Edition, Published 2003 Prentice Hall .
  6. [Jec97] Jech, T. J. : Set Theory, 2nd edn. Perspectives in Mathematical Logic. Springer, Berlin (1997).
  7. Chang C and Lee R, Symbolic Logic Mechanical Theorem proving, Academic press, New York, 1973.
  8. Nilsson N Principal of Artificial Intelligence, Tioga Publishing Company, 1980.
  9. Winston P H Artificial Intelligence, 2nd edition, Addison-Wesley, Menlo-Park, California, 1984.
  10. Foundation of artificial intelligence and expert system by Janakiraman.
  11. Artificial intelligence,3rd edn, by Elaine Rich ,Kevin Knight, Shivashankar B Nair.
  12. Introduction to 'Artificial intelligence and expert system' by Dan W. Patterson, PHI
  13. Resolution By Ankit Shah, Professor Harper Langston Discrete Mathematics Summer 2007
  14. Artificial intelligence notes- reasoning methods, lecturer: Co?kun Sönmez
Index Terms

Computer Science
Information Sciences

Keywords

Resolution principle Substitution Unification complementary literals Skolemization

Powered by PhDFocusTM