Is this propositional formula an instance of an axiom?

Question

Please help me automate my discrete mathematics homework. Given a valid propositional formula, check if it is an instance of one of Łukasiewicz's axioms. Here's how it works.

A term can be defined inductively as follows:

• Single lower-case letters of the Latin alphabet (a, b, c, etcetera) are terms.
• Given a term ϕ, ¬ϕ is also a term.
• Given terms ϕ and ψ, (ϕ→ψ) is also a term.

A formula is itself a term, usually made up of smaller terms. An example of a formula is (a→b)→¬(¬c→¬¬a).

Now, these are the three axioms. They are formula templates; some formulae are instances of an axiom. You make an instance by replacing all the variables (the Greek letters) with terms.

A: ϕ→(ψ→ϕ)
B: (ϕ→(ψ→χ))→((ϕ→ψ)→(ϕ→χ))
C: (¬ϕ→¬ψ)→(ψ→ϕ)

Same Greek letters have to be substituted with the same terms. Thus, one instance of the axiom A is (b→¬c)→(c→(b→¬c)). In this case ϕ has been substituted with (b→¬c), and ψ with c. Key to solving problems or making proofs in propositional logic is recognising when formulae are instances of axioms.

Note that all these axioms have their outer parens stripped away, which is common to do on the highest level. The strict way to write these is (ϕ→(ψ→ϕ)) ((ϕ→(ψ→χ))→((ϕ→ψ)→(ϕ→χ))) ((¬ϕ→¬ψ)→(ψ→ϕ)), with surrounding parens, but people usually leave those out when the meaning is clear so I'll leave it free how you choose to parse them.

The goal of the program is to take as input a valid formula in string or character array format, and output A, B or C (upper or lower case is fine) if it is an instance of the respective axiom, and do something else (output zero, output nothing, basically do anything except throwing an error) if it is not. The question is code-golf; the shortest code wins!

Test cases

input; output
(a→(a→a))→((a→a)→(a→a)); B
(a→(b→¬¬¬¬¬c))→((a→b)→(a→¬¬¬¬¬c)); B
(¬¬¬x→¬z)→(z→¬¬x); C
(¬(a→(b→¬c))→¬(c→c))→((c→c)→(a→(b→¬c))); C
(b→¬c)→(c→(b→¬c)); A
a→(b→c); 0

Alternatively, with surrounding parentheses:

input; output
((a→(a→a))→((a→a)→(a→a))); B
((a→(b→¬¬¬¬¬c))→((a→b)→(a→¬¬¬¬¬c))); B
((¬¬¬x→¬z)→(z→¬¬x)); C
((¬(a→(b→¬c))→¬(c→c))→((c→c)→(a→(b→¬c)))); C
((b→¬c)→(c→(b→¬c))); A
(a→(b→c)); 0

If you want to stick with printable ascii characters, you can use > for → and ! for ¬:

input; output
(a>(a>a))>((a>a)>(a>a)); B
(a>(b>!!!!!c))>((a>b)>(a>!!!!!c)); B
(!!!x>!z)>(z>!!x); C
(!(a>(b>!c))>!(c>c))>((c>c)>(a>(b>!c))); C
(b>!c)>(c>(b>!c)); A
a>(b>c); 0

Alternatively, with surrounding parentheses:

input; output
((a>(a>a))>((a>a)>(a>a))); B
((a>(b>!!!!!c))>((a>b)>(a>!!!!!c))); B
((!!!x>!z)>(z>!!x)); C
((!(a>(b>!c))>!(c>c))>((c>c)>(a>(b>!c)))); C
((b>!c)>(c>(b>!c))); A
(a>(b>c)); 0

Answer 1

Curry (PAKCS), 175 bytes

n s='!':s
s%t='(':s++'>':t++")"
p[a]|a>'`'=1
p(n s)=p s
p(s%t)=p s*p t
f(a++'>':b%a)|p a==p b="A"
f(a%(b%c)++'>':(a%b)%(a%c))|p a*p b==p c="B"
f(n a%n b++'>':b%a)|p a==p b="C"

Try it online!

Takes input in ASCII characters. Returns nothing if it is not an axiom.

Answer 2

Pip, 99 83 bytes

(AZ'^.("9>,9>\1
,9>,9>9  >,,\1>\2 >,\1>\3 
,!9>!9 >,\2>\1"R9C+XX^n).` $`NaTRpk@?:1)

Attempt This Online!

Explanation

A lightly compressed regex solution.

First, we're going to modify the input a bit:

aTRpk
a      Command-line argument
 TR    Transliterate
   p    from "()"
    k   to ", "

Using , in place of () saves bytes on backslashes in the regexes.

Next, we're going to construct a list containing the following three regexes for axioms A, B, and C respectively:

^(.+)>,.+>\1 $
^            $  The full string must match
 (.+)           Match any run of characters (capture group 1)
     >,         →(
       .+       Match any run of characters
         >      →
          \1    Match group 1 again
            ␠   )

^,(.+)>,(.+)>(.+)  >,,\1>\2 >,\1>\3  $
^                                    $  The full string must match
 ,                                      (
  (.+)                                  Match any run of characters (capture group 1)
      >,                                →(
        (.+)                            Match any run of characters (capture group 2)
            >                           →
             (.+)                       Match any run of characters (capture group 3)
                 ␠␠>,,                  ))→((
                      \1                Match group 1 again
                        >               →
                         \2             Match group 2 again
                           ␠>,          )→(
                              \1        Match group 1 again
                                >       →
                                 \3     Match group 3 again
                                   ␠␠   ))

^,!(.+)>!(.+) >,\2>\1 $
^                     $  The full string must match
 ,!                      (¬
   (.+)                  Match any run of characters (capture group 1)
       >!                →¬
         (.+)            Match any run of characters (capture group 2)
             ␠>,         )→(
                \2       Match group 2 again
                  >      →
                   \1    Match group 1 again
                     ␠   )

We start with this string:

"9>,9>\1
,9>,9>9  >,,\1>\2 >,\1>\3 
,!9>!9 >,\2>\1"

Then:

'^.("..."R9C+XX^n).` $`
    "..."                The above string
         R9              Replace each 9 with:
             XX            Regex `.`
            +              Apply + quantifier: `.+`
           C               Wrap in capture group: `(.+)`
               ^n        Split the resulting string on newlines
'^.                      Concatenate "^" to the front
                 .` $`   Concatenate ` $` to the end, coercing the result to a regex

Now we use the N operator to count the number of matches of each of these regexes in the transliterated input. The result will be a list of 0's and 1's: [1 0 0] if the first regex matched, [0 1 0] if the second matched, [0 0 1] if the third matched, or [0 0 0] if none matched.

Finally:

(AZ...@?:1)
   ...       That three-element list
      @?:    Find the index of the first occurrence of
         1   1
(AZ       )  Use that number to index into the uppercase alphabet
             If 1 is not found, returns nil, which results in no output

Answer 3

Python3, 450 bytes:

lambda t,y:next((b for a,b in t if all(c(a,p(y)[0],{}))),0)
T=type
def p(s,c=0):
 q,n=[],0
 while s and(c==0 or s[0]!=')'):
  n+=(S:=s[0])=='!'
  if S.isalpha():q+=[[n,S]];n=0
  if S=='(':t,s=p(s[1:],1);q+=[(n,t)];n=0
  s=s[1:]
 return q,s
def c(a,b,d):
 if T(a)!=T(b):return
 for x,y in zip(a,b):
  p,q=x;n,m=y
  if(t:=T(x))==list:yield all([d.get(q,m)==m,not p or p%2==n%2]);d[q]=m
  if t==tuple:yield all([T(y)==tuple,not p or p%2==n%2,*c(q,m,d)])

Try it online!

Answer 4

Retina 0.8.2, 102 bytes

T`()`{}
{((.+)>{.+>\2}|(.+)>{(.+)>(.+)}}>{{\3>\4}>{\3>\5}|!(.+)>!(.+)}>{\7>\6)}$|.+
$#2$*A$#4$*B$#6$*C

Try it online! Link includes test cases. Outputs nothing unless the input is one of the axioms. Explanation: Another regex-based answer.

T`()`{}

Translate the ()s to {}s to avoid 14 \s.

{((.+)>{.+>\2}|(.+)>{(.+)>(.+)}}>{{\3>\4}>{\3>\5}|!(.+)>!(.+)}>{\7>\6)}$|.+

Try to match one of the three axioms, but if there isn't an immediate match then just match everything.

$#2$*A$#4$*B$#6$*C

Output the corresponding letter if one of the capture groups in the relevant axiom exists. (Axiom A only has one capture group but for the others any representative capture group works.)

Answer 5

PERL, 116114 bytes

#!/usr/bin/perl -p
y/()/XY/;s/^(.+)>X(.+)>\1Y$/A/;s/(X.+>)X(.+)>(.+YY)>X\1\2Y>\1\3$/B/;s/X!(.+)>!(.+)Y>X\2>\1Y/C/

This comes with a shebang line, so is suitable for a standalone executable script. If you are willing to execute it as perl -p scriptfilename, the shebang line can be dropped, or to execute as perl scriptfilename, the shebang line can be replaced with a final ;print

The behaviour for the "not an axiom instance" case is to print the input with parentheses replaced by X and Y, respectively. This certainly counts as "do something else" because this output is guaranteed to be different from A, B, C (e.g., it is guaranteed to contain a lowercase letter)