A Drag-and-Drop Proof Tactic

2025-04-30 0 0 954.5KB 13 页 10玖币

侵权投诉

Pablo Donato

pablo.donato@polytechnique.edu

École polytechnique

LIX

France

Pierre-Yves Strub

pierre-yves.strub@polytechnique.edu

École polytechnique

LIX

France

Benjamin Werner

benjamin.werner@polytechnique.edu

École polytechnique

LIX

France

Abstract

We explore the features of a user interface where formal

proofs can be built through gestural actions. In particular,

we show how proof construction steps can be associated to

drag-and-drop actions. We argue that this can provide quick

and intuitive proof construction steps. This work builds on

theoretical tools coming from deep inference. It also resumes

and integrates some ideas of the former proof-by-pointing

project.

CCS Concepts: •Mathematics of computing →

Mathe-

matical software;

•Human-centered computing →

Graph-

ical user interfaces;Gestural input;

•Theory of computa-

tion →

Proof theory;Equational logic and rewriting;Con-

structive mathematics.

Keywords:

logic, formal proofs, user interfaces, deep infer-

ence

ACM Reference Format:

Pablo Donato, Pierre-Yves Strub, and Benjamin Werner. 2022. A

Drag-and-Drop Proof Tactic. In Proceedings of the 11th ACM SIG-

PLAN International Conference on Certied Programs and Proofs

(CPP ’22), January 17–18, 2022, Philadelphia, PA, USA. ACM, New

York, NY, USA, 13 pages. hps://doi.org/10.1145/3497775.3503692

1 Introduction

Most Interactive Theorem Provers allow the user to incre-

mentally construct formal proofs through an interaction loop.

One progresses through a sequence of states corresponding

to incomplete proofs. Each of these states is itself described

by a nite set of goals and the proof is completed once there

are no goals left. From the user’s point of view, a goal ap-

pears as a sequent, in the sense coined by Gentzen. In the

case of intuitionistic logic that is:

Permission to make digital or hard copies of all or part of this work for

personal or classroom use is granted without fee provided that copies are not

made or distributed for prot or commercial advantage and that copies bear

this notice and the full citation on the rst page. Copyrights for components

of this work owned by others than ACM must be honored. Abstracting with

credit is permitted. To copy otherwise, or republish, to post on servers or to

redistribute to lists, requires prior specic permission and/or a fee. Request

permissions from permissions@acm.org.

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

ACM ISBN 978-1-4503-9182-5/22/01. .. $15.00

hps://doi.org/10.1145/3497775.3503692

•

One particular proposition

𝐴

which is to be proved; we

designate it as the goal’s conclusion,

•a set of propositions Γcorresponding to hypotheses.

On paper, this sequent is written

Γ⊢𝐴

. The user performs

actions on one such goal at a time, and the actions transform

the goal, or rather replace the goal by a new set of goals.

When this set is empty, the goal is said to be solved.

The actions performed by the user can be more or less

sophisticated. But, fundamentally, one nds elementary com-

mands which correspond roughly to the logical rules, gen-

erally of natural deduction. For instance, a goal

Γ⊢𝐴∨𝐵

(resp.

Γ⊢𝐴∧𝐵

) can be turned into either a goal

Γ⊢𝐴

or a

goal Γ⊢𝐵(resp. into two goals Γ⊢𝐴and Γ⊢𝐵).

To sum up, during the proof construction process, a state

is a set of sequents. These goals/sequents are modied by

commands, which allow the user to navigate from the original

statement of the theorem to the state where there are no

goals left to be proved.

In the dominant paradigm, these commands are provided

by the user in text form; since Robin Milner and LCF [

they are called tactics. Proof les are literally proof-scripts;

that is the sequence of tactics typed-in by the user.

The present work is a form of continuation of the Proof-by-

Pointing (PbP) eort, initiated in the 1990’s by Gilles Kahn,

Yves Bertot, Laurent Théry and their group [

]. Both works

share a main idea which is to replace the textual tactic com-

mands by gestural actions performed by the user on a graph-

ical user interface. In both cases, the items the user performs

actions on are the current goal’s conclusion and hypotheses.

What is new in our work is that we allow not only to click on

(subterms of) these items, but also to move them in order to

drag-and-drop (DnD) one item onto another. This enriches

the language of actions in, we argue, an intuitive way. We

should point out that what is proposed here is not meant to

replace but to complement the proof-by-pointing features.

We thus envision a general proof-by-action paradigm, which

includes both PbP and DnD features.

In this article, we focus on how drag-and-drop actions

implement proof construction operations corresponding to

the core logic; that is how they deal with logical connectives,

quantiers and equality. We have started to implement this in

a prototype named Actema (for Active Mathematics) running

through a web HTML5/JavaScript interface. This possibility

to experiment in practice, even though yet on a small scale,

gave valuable feedback for crafting the way DnD actions are

arXiv:2210.11820v2 [cs.HC] 7 Nov 2022

CPP ’22, January 17–18, 2022, Philadelphia, PA, USA Pablo Donato, Pierre-Yves Strub, and Benjamin Werner

to be translated into proof construction steps in an intuitive

and practical way.

The rest of this article is organized as follows. Section 2ex-

plains the motivations behind this work, and section 3briey

outlines its logical setting. Section 4describes the basic fea-

tures of a graphical proof interface based on our principles,

and illustrates them with a famous syllogism from Aristotle.

Section 5shows how it can integrate basic proof-by-pointing

capabilities. The next two sections explain, through further

examples, how the drag-and-drop paradigm works; rst for

so-called rewrite actions involving equalities, then for ac-

tions involving logical connectives and quantiers. Section 8

introduces the notions of context and polarity, in order to

prove the correctness of our system. Section 9explains how

DnD actions are specied by the user interactively, through

schemas called linkages. Section 10 describes how linkages

translate into logical steps, as well as some properties of

this translation. Section 11 studies a proof of a small logical

riddle in Actema, highlighting some benets of our approach

compared to textual systems. We end with a discussion on

some related works in section 12, and then conclude.

2 Motivations

Since this work is about changing the very way the user

interacts with an interactive theorem prover, we feel it is

important to make some disclaimers about the aims and the

scope of what is presented here.

From a development point of view, we are still at a very

preliminary stage. Building a real-size proof system integrat-

ing the ideas we present would require an important eort

and is still a long term goal. Some concepts however have

emerged, which, we hope allow to sketch some aspects of

the look-and-feel of such a system, and what some of its

advantages could be.

Also, at this stage, we focus on basic proof constructions

and on how the gestural approach can help make them more

ecient and more intuitive. Some of the illustrative examples

we give below could probably be dealt with using advanced

proof search tactics, but we believe this does not make them

irrelevant. Rather than (sub)goals to be proved, these exam-

ples should be seen as generic situations often encountered

in the course of a proof, which require small and local trans-

formations to the statements involved.

The idea of interactive theorem provers is that automation

and user actions complement each other, and we here focus

on the latter for the time being. The question of integrat-

ing drag-and-drop actions and powerful proof automation

techniques is left for future work.

Finally, precisely because our approach is about giving the

user a smoother control of the proof construction process,

we see a possibility for our work to help making future proof

systems more suited for education.

3 Logical Setting

Any proof system must implement a given logical formalism.

What we describe here ought to be applied to a wide range

of formalisms, but in this article we focus on the core of in-

tuitionistic rst-order logic with equality (FOL). This allows

us to consider sequents where hypotheses are unordered

which, in turn, simplies the technical presentations. We

will thus write

Γ, 𝐴 ⊢𝐵

for a sequent where

𝐴

is among the

hypotheses.

We use and do not recall the usual denitions of terms

and propositions in rst order logic. We assume a rst order

language (function and predicate symbols) is given. Provabil-

ity is dened over sequents

Γ⊢𝐴

by the usual logical rules

of natural deduction (NJ) and/or sequent calculus (LJ).

Equality is treated in a common way:

is a binary pred-

icate symbol written in the usual inx notation, together

with the reexivity axiom

∀𝑥.𝑥 =𝑥

and the Leibniz scheme,

stating that for any proposition 𝐴one has

∀𝑥.∀𝑦.𝑥 =𝑦∧𝐴⇒𝐴[𝑥\𝑦].

We will not consider, on paper, the details of variable

renaming in substitutions, implicitly applying the so-called

Barendregt convention, that bound and free variables are

distinct and that a variable is bound at most once.

Extending this work to simple extensions of FOL, like

multi-sorted predicate calculus is straightforward (and ac-

tually done in the prototype). Some more interesting points

may show up when considering how to apply this work to

more complex formalisms like type theories. We will not

explore these questions here.

Another interesting and promising question is how our ap-

proach extends to classical logic(s), that is multi-conclusion

classical sequents. In this text we only give a few hints on

this topic.

4 A First Example

4.1 Layout

One advantage of the proof-by-actions paradigm, is that it

allows a very lean visual layout of the proof state. There is

no need to name hypotheses. In the prototype we also dis-

pense with a text buer, since proofs are solely built through

graphical actions.

Figure 1shows the layout of the system using the ancient

example of Aristotle. A goal appears as a set of items whose

nature is dened by their respective colors1:

•

Ared item which is the proposition to be proved, that

is the conclusion,

•blue items, which are the local hypotheses.

We are well aware that, in later implementations, this color-based distinc-

tion ought to be complemented by some other visual distinction, at least

for users with impaired color vision. But in the present description we stick

to the red/blue denomination, as it is conveniently concise.

A Drag-and-Drop Proof Tactic CPP ’22, January 17–18, 2022, Philadelphia, PA, USA

Figure 1.

A partial screenshot showing a goal in the Actema prototype. The conclusion is red on the right, the two hypotheses blue on the

left. The grey dotted arrows have been added to show the two possible actions.

The items are what the user can act upon: either by clicking

on them, or by moving them.

Finally, note that each goal is displayed on a tab.

4.2 Two Kinds of Actions

In this example, there are two possible actions.

•

A rst one is to bring together, by drag-and-drop, the

red conclusion

Mort(Socr)

with the succedant of the

rst hypothesis

Mort(𝑥)

. This will transform the goal

by changing the conclusion to Hum(Socr).

•

A second possibility is to combine the two hypotheses;

more precisely to bring together the item

Hum(Socr)

with the premise

Hum(𝑥)

of the rst hypothesis. This

will yield a new hypothesis Mort(Socr).

The rst case is what we call a backward step where the

conclusion is modied by using a hypothesis. The second

case is a forward step where two known facts are combined

to deduce a new fact, that is an additional blue item.

In both cases, the proof can then be nished invoking

the logical axiom rule. In practice this means bringing to-

gether the blue hypothesis

Hum(Socr)

(resp. the new blue

fact Mort(Socr)) with the red goal.

4.3 Modeling the Mechanism

A backward step involves a hypothesis, here

∀𝑥.Hum(𝑥) ⇒

Mort(𝑥)

and the conclusion, here

Mort(Socr)

. Furthermore,

the action actually links together two subterms of each of

these items; this is written by squaring these subterms. The

symbol

⊢

, used as an operator, is meant to describe the result

of the interaction. Internally, the behavior of this operator is

dened by a set of rewrite rules given in gures 3and 4. Here

is the sequence of rewrites corresponding to the example

∀𝑥.Hum(𝑥) ⇒ Mort(𝑥) ⊢ Mort(Socr)

▷Hum(Socr) ⇒ Mort(Socr) ⊢ Mort(Socr)L∀i

▷Hum(Socr)∧(Mort(Socr) ⊢ Mort(Socr) ) L⇒2

▷Hum(Socr) ∧ ⊤ id

▷Hum(Socr)neur

Notice that:

•

These elementary rewrites are not visible for the user.

What she/he sees is the nal result of the action, that

is the last expression of the rewrite sequence.

•

The denitions of the rewrite rules in gures 3and 4

do not involve squared subterms. The information of

which subterms are squared is only used by the system

to decide which rules to apply in which order.

In general, the action solves the goal when the interaction

ends with the trivially true proposition

⊤

. The base case

being the action corresponding to the axiom/identity rule

𝐴⊢𝐴▷⊤.

A forward step, on the other hand, involves two (subterms

of two) hypotheses. The interaction operator between two

hypotheses is written

∗

. In the example above, the detail of

the interaction is:

∀𝑥. Hum(𝑥) ⇒ Mort(𝑥) ∗ Hum(Socr)

▷Hum(Socr) ⇒ Mort(Socr) ∗ Hum(Socr)F∀i

▷(Hum(Socr) ⊢ Hum(Socr) ) ⇒ Mort(Socr)F⇒1

▷⊤ ⇒ Mort(Socr)id

▷Mort(Socr)neul

The nal result is the new hypothesis.

We come back to the study of the rewrite rules of

⊢

and

∗

further down.

2Note that ⊢has lower precedence than all logical connectives.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

ADrag-and-DropProofTacticPabloDonatopablo.donato@polytechnique.eduÉcolepolytechniqueLIXFrancePierre-YvesStrubpierre-yves.strub@polytechnique.eduÉcolepolytechniqueLIXFranceBenjaminWernerbenjamin.werner@polytechnique.eduÉcolepolytechniqueLIXFranceAbstractWeexplorethefeaturesofauserinterfacewhereformal...

展开>> 收起<<

A Drag-and-Drop Proof Tactic.pdf

共13页,预览3页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

A Drag-and-Drop Proof Tactic

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: