2021-01-12 12:36:35 (GMT)
Hi all,
I went through the problems that are (relatively) easily solvable by Satallax and CVC4 and I noticed one thing: most of them have something to do with finite domains.
Is anyone aware of techniques to support finite domains better in superposition provers?
Finite domain axioms are absolutely horrible as Vampire people showed with FOOL work.
As for HO aspects of finite domains, we can simply enumerate all functions that operate on finite domains and it seems that on some smaller problems this might help.
I will investigate this and let you all know.
Cheers
Petar
2021-01-12 12:41:33 (GMT)
There is this paragraph in the first FOOL paper:
Efficient superposition theorem proving in finite domains, such as the boolean domain, is also discussed in [9]. The approach of [9] sometimes falls back to enumerating instances of a clause by instantiating finite domain variables with all elements of the corresponding domains. We point out here that for the boolean (i.e., two-element) domain there is a simpler solution. However, the approach of [9] also allows one to handle domains with more than two elements. One can also generalise our approach to arbitrary finite domains by using binary encod- ings of finite domains, however, this will necessarily result in loss of efficiency, since a single variable over a domain with 2^k elements will become k variables in our approach, and similarly for function arguments.
And [9] is:
Hillenbrand, T., Weidenbach, C.: Superposition for bounded domains. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 68–100. Springer, Heidelberg (2013)
2021-01-12 12:51:2 (GMT)
I skimmed through 9 and it seemed way too complicated and still requires you to introduce some axioms
2021-01-12 12:51:4 (GMT)
Thanks anyway
2021-01-12 12:53:11 (GMT)
What about the binary encoding that the FOOL paper proposes?
2021-01-12 12:56:40 (GMT)
if I understand correctly
2021-01-12 12:58:40 (GMT)
this means that if you have a domain of cardinality N, 2^k <= N < 2^k+1
you would create a fresh Nary symbol f where each argument is of boolean type
2021-01-12 12:59:20 (GMT)
to represent different eleements of the domain?
2021-01-12 12:59:50 (GMT)
so 0-th element would be represented by f(false, false, ..., false) and the last element with f(true, true, ..., true)?
2021-01-12 13:1:42 (GMT)
Yeah, that might be what they mean.
2021-01-12 13:2:29 (GMT)
OK, I will work on this today together with enumeration of boolean functions
2021-01-12 13:3:32 (GMT)
thanks
2021-01-12 14:49:19 (GMT)
Petar Vukmirovic said:
Hi all,
I went through the problems that are (relatively) easily solvable by Satallax and CVC4 and I noticed one thing: most of them have something to do with finite domains.
Is anyone aware of techniques to support finite domains better in superposition provers?
Finite domain axioms are absolutely horrible as Vampire people showed with FOOL work.As for HO aspects of finite domains, we can simply enumerate all functions that operate on finite domains and it seems that on some smaller problems this might help.
I will investigate this and let you all know.Cheers
Petar
there is a module for finite domains in Zipperposition, it just needs to detect axioms :-)
2021-01-12 14:49:52 (GMT)
At least to prevent self-superposition of the finite domain axioms, because that's horribly expensive.
2021-01-12 14:50:22 (GMT)
src/prover_calculi/enumTypes
2021-01-12 14:54:36 (GMT)
once again it needs to be freshen up… :sweat_smile:
2021-01-12 15:0:2 (GMT)
enumerating the functions on the finite domain for HO unif is an interesting idea!
2021-01-12 16:8:55 (GMT)
ok thanks a lot I will give it a look!
2021-01-12 16:13:44 (GMT)
iirc it was added so we could saturate on problems like …
2021-01-12 16:39:30 (GMT)
These are exactly the things we should address in the system description
2021-01-12 16:39:41 (GMT)
when you have the time we can skype and write a list of things to be in this doc
2021-01-12 16:46:9 (GMT)
Sounds good!
2021-01-12 16:46:33 (GMT)
tbh that'd be best done by looking at the code base so I can remember what's where :joy:
2021-01-12 16:49:56 (GMT)
sure, I agree
2021-01-12 17:1:25 (GMT)
what would be a good time for you?
2021-01-12 17:6:1 (GMT)
Thursday or Friday any time
2021-01-12 17:18:23 (GMT)
how about friday? at noon here (so 6pm for you I think?)
2021-01-12 17:19:33 (GMT)
Let's do it