First Order Logic in Semantic Tableau and VAMPIRE
Journal: International Journal of Engineering Sciences & Research Technology (IJESRT) (Vol.3, No. 9)Publication Date: 2014-09-30
Authors : Rania Mahmoud; Ismail Amr Ismail; Ahmed Fahim;
Page : 528-534
Keywords : Predicate Logic; Semantic Tableau; 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.
Other Latest Articles
- Performance Enhancement of Sugar Mill by Alternate Cooling System for Condenser
- Sybil Attack in Vanet by Neighbourhood Information Passing
- Comparative Analysis of Various Condenser in Vapour Compression Refrigeration System
- A Survey on Data Processing Protocols in Wireless Sensor Network
- Conversion of selected waste Plastic in to Synthetic Fuel (Synthetic Diesel)
Last modified: 2014-10-16 22:21:02