Predicate solving

[Cypher1]

Is your feature request related to a problem? Please describe.
Current triples can only be combined when their preconditions and postconditions match.
These matches are unnecessarily restrictive and do not support rewriting or reasoning.

Describe the solution you'd like
I propose that conditions be 'solved' rather than simply checked, using a search based rewriting strategy similar to Prolog's query resolution algorithm.
This should allow expressive pre+post-conditions that can express more clearly the requirements that a function has without requiring users to manually promise that things are safe (without any actual checking).

Describe alternatives you've considered
One alternative would be having Coq style expressions that are added in the process of 'merging' two triples that mutate the pre/post conditions until there is a match or a failure. This would lead to writing proofs that functions could be run in others contexts which may be hard to reason about.

Also, Coq already does this quite well.

I have yet to find another alternative.

Additional context

Unfortunately this requires the addition of 'unknown variables' or placeholders that are not explicitly specified and inference rules for resolving predicates. This complicates the symbol and predicate models.

e.g. {?x, ?y, ?z, isa, ?x isa ?y, ?y isa ?z}[]{?x isa ?z} allows the program to reason about the isa relationship.