Embedding and Automating Conditional Logics in Classical Higher-Order Logic

2011/06/18 by Benzmueller, Christoph, Gabbay, Dov, Genovese, Valerio +1
#03B15 #03B60 #68T15 #68T27 #68T30 #Artificial Intelligence (cs.AI) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #I.2.0 #I.2.3 #I.2.4 #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1106.3685

Abstract

A sound and complete embedding of conditional logics into classical higher-order logic is presented. This embedding enables the application of off-the-shelf higher-order automated theorem provers and model finders for reasoning within and about conditional logics.

Related

• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
• Quantified Conditional Logics are Fragments of HOL
• I/O Logic in HOL --- First Steps
• Faithful Logic Embeddings in HOL -- Deep and Shallow
• Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study