Implementing the First-Order Logic of Here and There
We present automated theorem provers for the first-order logic of here and there (HT). They are based on a native sequent calculus for the logic of HT and an axiomatic embedding of the logic of HT into intuitionistic logic. The analytic proof search in the sequent calculus is optimized by using free variables and skolemization. The embedding is used in combination with sequent, tableau and connection calculi for intuitionistic first-order logic. All provers are evaluated on a large benchmark set of first-order formulas, providing a foundation for the development of more efficient HT provers.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Analysis of Dialogical Argumentation via Finite State Machines
Dialogical argumentation is an important cognitive activity by which agents exchange arguments and counterarguments as part of some process such as discussion, debate, persuasion and negotiation. Whilst numerous formal s…
Team Plan Recognition: A Review of the State of the Art
There is an increasing need to develop artificial intelligence systems that assist groups of humans working on coordinated tasks. These systems must recognize and understand the plans and relationships between actions fo…
Computing FO-Rewritings in EL in Practice: from Atomic to Conjunctive Queries
A prominent approach to implementing ontology-mediated queries (OMQs) is to rewrite into a first-order query, which is then executed using a conventional SQL database system. We consider the case where the ontology is fo…
Discussion Graph Semantics of First-Order Logic with Equality for Reasoning about Discussion and Argumentation
We formulate discussion graph semantics of first-order logic with equality for reasoning about discussion and argumentation as naturally as we would reason about sentences. While there are a few existing proposals to use…
Formal LogicStrength Factors: An Uncertainty System for a Quantified Modal Logic
We present a new system S for handling uncertainty in a quantified modal logic (first-order modal logic). The system is based on both probability theory and proof theory. The system is derived from Chisholm's epistemolog…
counterfactual