cardTAP: Automated Deduction on a Smart Card

We present the rst implementation of a theorem prover which runs on a smart card. The prover is written in Java and implements a dual tableau calculus.1 Due to the limited resources available on current smart cards, the prover is restricted to propositional classical logic. It can be easily extended to full rst-order logic. The potential applications for our prover lie within the context of security related functions based on trusted devices such as smart cards.

• Type: Conference
• Year: 1998
• Where: AUSAI
• Authors: Andrew Slater, Rajeev Goré, Joachim Posegga, Harald Vogt
• Keywords: Artificial Intelligence, AUSAI 1998, Prover, Smart Cards, Theorem Prover