| Autor: |
Paulo A. S. Veloso, Sheila R. M. Veloso |
| Jazyk: |
angličtina |
| Rok vydání: |
2013 |
| Předmět: |
|
| Zdroj: |
Electronic Proceedings in Theoretical Computer Science, Vol 113, Iss Proc. LSFA 2012, Pp 153-168 (2013) |
| Druh dokumentu: |
article |
| ISSN: |
2075-2180 |
| DOI: |
10.4204/EPTCS.113.15 |
| Popis: |
We introduce a refutation graph calculus for classical first-order predicate logic, which is an extension of previous ones for binary relations. One reduces logical consequence to establishing that a constructed graph has empty extension, i. e. it represents bottom. Our calculus establishes that a graph has empty extension by converting it to a normal form, which is expanded to other graphs until we can recognize conflicting situations (equivalent to a formula and its negation). |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
