First Order Logic in Semantic Tableau and VAMPIRE

Abstract

 Semantic tableau is a proof system used to prove the validity of a formula using Prolog, it can also be used to prove if a formula is a logic consequence of a set of formulas. Semantic tableau is used in both propositional and predicate logic. Tableau is a disjunction normal form. VAMPIRE is a high-performance theorem prover for first-order logic with or without equality. In this paper, a modified version of semantic tableau is presented, experimental results proved the validity of modified tableau. Also, it is shown how Tableau proof system and VAMPIRE can be used in predicate logic.

Authors and Affiliations

Mahmoud

Keywords

Related Articles

 Investigating the Hydrological Characteristics of Kaduna River Basin

 The water resource potential of the Kaduna River for use in irrigation development and water resource management has been studied. The water conveyance efficiencies of the river channels are very low that develop...

FCM Algorithm for Medical Image Segmentation Using HMRF

Clustering of data is a method by which large sets of data are grouped into clusters of smaller sets of similar data. Fuzzy c-means (FCM) clustering algorithm is one of the most commonly used unsupervised clustering te...

Simple and Cost-effective Heart Rate Meter Using PIC Microcontroller Simple and Cost-effective Heart Rate Meter Using PIC Microcontroller  

  One of the major and significant physiological parameters of human cardiovascular system is the heart rate. Heart rate is represented by the number of times the heart beats per minute. The heart rate data can ref...

EMPIRICAL DEMONSTRATION O F NEXT GENERATION HIGH SPEED HYBRID CMOS - SET B ASED CONSUMER FRIENDLY IBM MACHINE SUBSECTION

A t the very daw n of post CMOS era Single Electronics ushered new ventures in resolving power dissipation and power consumption like hindrances. Low power consuming, high speed & high...

 Optimizing Design of Spring Using Genetic Algorithm

 This paper deals with the elaborate design optimization technique of coil spring sets with genetic algorithm. Attention is focused on reducing the weight and stresses keeping into considerations the various critic...

Download PDF file
  • EP ID EP100722
  • DOI -
  • Views 98
  • Downloads 0

How To Cite

Mahmoud (30).  First Order Logic in Semantic Tableau and VAMPIRE. International Journal of Engineering Sciences & Research Technology, 3(9), 528-534. https://europub.co.uk/articles/-A-100722