Skip to content

Dp [Cfsn; LPO] is broken #5

@acertain

Description

@acertain

fails with Fatal error: exception Failure("Lpo.prec: unknown symbol p, 2").

cnf(assocm,axiom,( m(X,m(Y,Z)) = m(m(X,Y),Z) )).
cnf(sym_m,axiom,( m(X,Y) = m(Y,X) )).
cnf(unit_m,axiom,( m(one,X) = X )).

cnf(assoc_p,axiom,( p(X,p(Y,Z)) = p(p(X,Y),Z) )).
cnf(sym_p,axiom,( p(X,Y) = p(Y,X) )).
cnf(unit_p,axiom,( p(zero,X) = X )).

cnf(zero_m,axiom,( m(X,zero) = zero )).

cnf(dist,axiom,( m(X,p(Y,Z)) = p(m(X,Y),m(X,Z)) )).

with --complete-if-no-goal --kb should trigger it.

Actually afaict only Dp [Cfs] and Dp [Cfsn] work (not any other Dp config, and same for Dg & DgSucc).

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions