霍尔
计算机科学
编码(内存)
辩证法
语义学(计算机科学)
程序设计语言
高阶逻辑
证明助理
理论计算机科学
描述逻辑
人工智能
数学
认识论
哲学
几何学
数学证明
作者
Antoine Martina,Alexander Steen
标识
DOI:10.1093/logcom/exad079
摘要
Abstract An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant Isabelle/HOL. This approach allows for the computer-assisted analysis of abstract dialectical frameworks using automated and interactive reasoning tools within a uniform logic environment. Exemplary applications include the formal analysis and verification of meta-theoretical properties, and the generation of interpretations and extensions under specific semantic constraints.
科研通智能强力驱动
Strongly Powered by AbleSci AI