ebproof package incompatible

[mbertucci47]

The prooftree environment of ebproof is tagged as many formulas and parts, rather than a single block. Not sure what the correct tagging would be here.

\DocumentMetadata
  {
    lang=en-US,
    pdfversion=2.0,
    pdfstandard=ua-2,
    testphase={phase-III,math,title,table,firstaid}
  }
\documentclass{article}

\usepackage{ebproof}
\usepackage{xcolor}

\title{ebproof tagging test}

\begin{document}

\begin{prooftree}
\hypo{ \Gamma, A &\vdash B }
\infer1[abs]{ \Gamma &\vdash A\to B }
\hypo{ \Gamma \vdash A }
\infer2[app]{ \Gamma \vdash B }
\end{prooftree}

\bigskip

\begin{prooftree}
\hypo{ \Gamma &\vdash A }
\ellipsis{foo}{ \Gamma &\vdash A, B }
\end{prooftree}

\bigskip

\begin{prooftree}
\hypo{ \Gamma, A &\vdash B }
\infer1[abs]{ \Gamma &\vdash A\to B }
\rewrite{\color{red}\box\treebox}
\hypo{ \Gamma \vdash A }
\infer2[app]{ \Gamma \vdash B }
\end{prooftree}

\bigskip

\begin{prooftree}
\hypo{ A_1 \vee \cdots \vee A_n }
\hypo{ [A_i] }
\ellipsis{}{ B }
\delims{ \left( }{ \right)_{1\leq i\leq n} }
\infer2{ B }
\end{prooftree}

\end{document}

[FrankMittelbach]

your take on status @davidcarlisle ?

[davidcarlisle]

Hmm I think the tagging the terms as separate formulae isn't necessarily wrong although clearly it's currently lost all the structure ie the indivdual deduction steps denoted by the rules are essentially lost.

I think partially-compatible might be a better description than incompatible

[car222222]

Is this a case where a structure that is relatively straightforward to define in LaTeX has no obvious equivalent in any PDF namespace?

Or is it more simple: that it is clear how it should be tagged, but this is not yet done?

[davidcarlisle]

@car222222 I don't think there will ever be "one right way" to tag such things, a deduction proof like this is similar to commutative diagrams and other two dimensional layouts. For some purposes you'd want to ignore the visual layout and tag it to optimise a reading as a textual description of the proof, treating drawn rules as artifacts. For other purposes the tree layout is the main item under discussion or essential for understanding the following text and then you'd want to optimise a reading describing the layout. Of course just tagging the individual expressions with nothing representing their semantic or visual connections (the current outcome) is not ideal (but even that may be better than nothing)

[car222222]

Even better to support both/all such access types!

That is really the name of this game: to provide as much information as is needed (and present), not making bad/any choices.

Or not?

[FrankMittelbach]

Eventually, yes, that's the goal (to offer choices, but also to provide reasonable defaults so that things work well, most of the time without the need of manually making choices).

But we have to make a choice, both for the default or in fact for anything to implement initially, simply because it may not be possible to offer all conceivable coices up front. This is why we labeled it partially

And not making an initial choice and instead waiting to the point where you can offer all (sensible) variants is also making a choice, namely that nothing works until that point, so I think we are good in the sense that something works and we label it as to be reviewed at some point in the future.

[davidcarlisle]

As Frank said. I think an important thing to check for automatic tagging is that it doesn't make things worse, eg if the horizontal rules for proof deductions got tagged as fractions. (Which doesn't happen here) There will always be cases where additional markup will be needed for the highest quality tagging (alt texts for graphics being simplest example) but it is an important first step to check the baseline tagging if you just enable \DocumentMetadata partially-compatible seems a good classification here.