We present a novel application of Goal-Directed Answer Set Programming that
digitizes the model aircraft operator's compliance verification against the
Academy of Model Aircrafts (AMA) safety code. The AMA safety code regulates how
AMA flyers operate Unmanned Aerial Vehicles (UAVs) for limited recreational
purposes. Flying drones and their operators are subject to various rules before
and after the operation of the aircraft to ensure safe flights. In this paper,
we leverage Answer Set Programming to encode the AMA safety code and automate
compliance checks. To check compliance, we use the s(CASP) which is a
goal-directed ASP engine. By using s(CASP) the operators can easily check for
violations and obtain a justification tree explaining the cause of the
violations in human-readable natural language. Further, we implement an
algorithm to help the operators obtain the minimal set of conditions that need
to be satisfied in order to pass the compliance check. We develop a front-end
questionnaire interface that accepts various conditions and use the backend
s(CASP) engine to evaluate whether the conditions adhere to the regulations. We
also leverage s(CASP) implemented in SWI-Prolog, where SWI-Prolog exposes the
reasoning capabilities of s(CASP) as a REST service. To the best of our
knowledge, this is the first application of ASP in the AMA and Avionics
Compliance and Certification space.

本研究提出了一个应用目标导向答案集编程的新方法，以对模型飞行器的操作进行数字化，对其遵守学院模型飞行器安全规范进行验证。通过使用 s (CASP) 引擎，操作员可以轻松地检查违规行为并获得以人类可读的自然语言解释其原因的证明树。同时，为了帮助操作员通过合规检查，开发了一种前端问卷接口，接收各种条件，使用后端 s (CASP) 引擎评估这些条件是否符合相关规定。这是 ASP 在 AMA 和航空电子合规认证领域的首次应用。

利用面向目标的答案集规划自动批准无人机飞行准备

Automating UAV Flight Readiness Approval using Goal-Directed Answer Set Programming

Automated commonsense reasoning is essential for building human-like AI
systems featuring, for example, explainable AI. Event Calculus (EC) is a family
of formalisms that model commonsense reasoning with a sound, logical basis.
Previous attempts to mechanize reasoning using EC faced difficulties in the
treatment of the continuous change in dense domains (e.g., time and other
physical quantities), constraints among variables, default negation, and the
uniform application of different inference methods, among others. We propose
the use of s(CASP), a query-driven, top-down execution model for Predicate
Answer Set Programming with Constraints, to model and reason using EC. We show
how EC scenarios can be naturally and directly encoded in s(CASP) and how it
enables deductive and abductive reasoning tasks in domains featuring
constraints involving both dense time and dense fluents.

应用 s (CASP) 模型，演绎与缺省推理，对包括时间与数量等约束条件在内的领域进行事件演算。

使用目标导向约束答案集编程对事件演算进行建模与推理

Modeling and Reasoning in Event Calculus using Goal-Directed Constraint  Answer Set Programming

Ethical and legal concerns make it necessary for programs that may directly
influence the life of people (via, e.g., legal or health counseling) to justify
in human-understandable terms the advice given. Answer Set Programming has a
rich semantics that makes it possible to very concisely express complex
knowledge. However, justifying why an answer is a consequence from an ASP
program may be non-trivial -- even more so when the user is an expert in a
given domain, but not necessarily knowledgeable in ASP. Most ASP systems
generate answers using SAT-solving procedures on ground rules that do not match
how humans perceive reasoning. We propose using s(CASP), a query-driven,
top-down execution model for predicate ASP with constraints to generate
justification trees of (constrained) answer sets. The operational semantics of
s(CASP) relies on backward chaining, which is intuitive to follow and lends
itself to generating explanations that are easier to translate into natural
language. We show how s(CASP) provides minimal justifications for, among
others, relevant examples proposed in the literature, both as search trees but,
more importantly, as explanations in natural language. We validate our design
with real ASP applications and evaluate the cost of generating s(CASP)
justification trees.

使用基于约束的谓词应答集编程的查询驱动自顶向下执行模型 s (CASP) 生成完整解释树，为 ASP 应答集提供最小化且易于转化为自然语言的解释，显著促进了 ASP 程序理解和操作的可行性。