CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

The Inverse Method for Many-Valued Logics

Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Andrei Mantsivoda ; Andrei Voronkov
Proceedings of the 12th Mexican International Conference on Artificial Intelligence - Advances in Artificial Intelligence and Its Applications (MICAI 2013), November 24-30, 2013, Mexico City, Mexico. Felix Castro and Alexander F. Gelbukh and Miguel Gonzalez (editors), Springer Lectures Notes in Computer Science Vol. LNCS 8265 (2013), p. 12-23.
[Konferensbidrag, refereegranskat]

We define an automatic proof procedure for finitely many-valued logics given by truth tables. The proof procedure is based on the inverse method. To define this procedure, we introduce so-called introduction-based sequent calculi. By studying proof-theoretic properties of these calculi we derive efficient validity- and satisfiability-checking procedures based on the inverse method. We also show how to translate the validity problem for a formula to unsatisfiability checking of a set of propositional clauses.

Nyckelord: computational logic, proof theory, decision procedures, theorem proving, automated reasoning



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-01-07. Senast ändrad 2016-08-22.
CPL Pubid: 191598

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)