2020-05-01 12:28:11 (GMT)
@Michael Färber : AFAIK, Satallax has a rule that enumerates functions (of functions) that have Boolean domain and codomain.
For example , it will replace a binary Boolean symbol with all 16 possible binary boolean functions.
Can you explain how this rule works, how it scales to arbitrary arity functions and how useful it is? :slight_smile:
2020-05-01 12:28:22 (GMT)
@Alex Steen : Does Leo do something similar?
2020-07-08 0:30:30 (GMT)
(I'm looking at old topics for fun, please ignore if no longer relevant). I don't know about the systems above, but the best way I know to do this is enumerative syntax-guided synthesis, with pruning based on a strong rewriter and possibly using divide-and-conquer techniques to scale
2020-07-08 1:59:1 (GMT)
The piece that is missing to do synthesis, I think, is a (decidable, fast) criterion to know whether a given predicate instance is useful or not? In HO unif with primitive enumeration, I think you can't really know which instances will be useful, so you keep them until a subset of them leads to a proof. (I imagine synthesis here means something like counter-example guided syntactic refinement)
2020-07-08 2:11:18 (GMT)
(although: I guess you could use avatar(-lite) to allocate a boolean literal for each instance, that means "this instance is useful", and somehow manage to eliminate some of these branches… E.g. if you instantiate with , then the condition is false because of the instance , so you can cut the branch with the boolean literal )
2020-07-08 12:37:30 (GMT)
By "synthesis" I meant more "syntax-guided enumeration", which is what would be useful here. The part that depends on having criteria to know whether a value is useful does not necessarily apply (it's as if in the synthesis formulation you had no conjecture).
2020-07-08 12:39:34 (GMT)
Taking care of the predicate being useful or not can be done by the rest of the solver by generating "instantaition lemmas"
2020-07-08 12:39:38 (GMT)
as you describe above