First Order Logic in Semantic Tableau and VAMPIRE
Journal Title: International Journal of Engineering Sciences & Research Technology - Year 30, Vol 3, Issue 9
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
- EP ID EP100722
- DOI -
- Views 106
- Downloads 0
DATA STORAGE SECURITY IN CLOUD COMPUTING USING THIRD PARTY AUDITOR (TPA)
Cloud Computing is evolving and considered next generation architecture for computing. Typically cloud computing is a combination of computing recourses accessible via internet. Historically the client or organisat...
Isolation And Characterization Of Proteolytic Bacteria And Its Protease
Soil samples from different habitats like river, garden, garbage dumping areas were collected. These samples were screened for the presence of proteolytic bacteria. The isolates were selected on the isolates forming la...
NTELLIGENT OPTIMIZATION AND SCHEDULING OF NETWORKED CONTROL SYSTEMS USING NEURAL NETWORK
This paper presents the use of Neural Networks (NN) for transmission time scheduling for the Networked Control System (NCS) where a network is widely used to connect sensors and actuators to the control systems. T...
DESIGN OF STEPPED IMPEDANCE LOW PASS FILTER AT 2.4GHz
In this era, life can't be envisioned without wireless communication. The microwave filter is a component which gives frequency selectivity in mobile, radar, satellite communication systems working at microwav...
Devanagari Handwritten Numeral Recognition Using Probabilistic Neural Network
In the last half century, the English character recognition was studied and the results were of such type that’s it can produce technology driven applications. But the same approach cannot be used in case of India...