5
Czy Z3 może generować interpolanty Craiga (przynajmniej dla logiki zdaniowej?). Nie znalazłem tego w dokumentacji Z3.Czy obsługa Z3 Interpolacja Craiga
A
Odpowiedz
4
Nie, Z3 nie obsługuje interpolantów Craig, ale generuje dowody. Interpolanty można wyodrębnić z dowodów. Ken Mcmillan opracowuje generator interpolantowy na Z3 przy użyciu tego podejścia.
Powiązane problemy
- 1. Obsługa kwantyfikatora Z3
- 2. Czy Z3 może pracować w trybie przyrostowym?
- 3. QF_FPA? Czy Z3 obsługuje arytmetykę IEEE-754?
- 4. Biegunowość Z3 za pomocą Z3 jako SAT Solver
- 5. Wynik kontrprzykładu Z3
- 6. Czytaj func interp tablicy z3 z modelu z3
- 7. Python interpolacja
- 8. interpolacja String
- 9. Jak ukryć zmienną Z3
- 10. z3 C++ API & ite
- 11. kwantyfikatorów w Z3
- 12. Różnica między Z3 i coq
- 13. Skalowanie/interpolacja UIImageView
- 14. Z3: znajdowanie wszystkich satysfakcjonujących modeli
- 15. zmiennej interpolacja w VB.NET
- 16. Interpolacja logarytmiczna w pythoniu
- 17. interpolacja String o zmiennej
- 18. Interpolacja na wykresach kubizmu
- 19. Sprawdź przepełnienie za pomocą Z3
- 20. Interpolacja dwuliniowa SSE
- 21. Interpolacja linii w Qt?
- 22. Czy Z3 może być używany do wnioskowania o podciągach?
- 23. Czy liczenie odwołań Z3_ast zawiera odniesienia poza Z3?
- 24. Czy Z3 może być używany do wstępnego przetwarzania problemów?
- 25. Interpolacja w pojedynczych cudzysłowach
- 26. Interpolacja w JavaScript
- 27. C# Interpolacja liniowa
- 28. Ruby, Interpolacja tablicę łańcuchów
- 29. R levelplot i interpolacja
- 30. Interpolacja kolorów OpenGL
Dziękuję za odpowiedź. Czy wiesz o statusie projektu? Czy skończy się za kilka dni, tygodni, miesięcy? –
Procedura decyzyjna interpolacji Kena jest już używana. W końcu udostępni go na stronie internetowej MSR. Na razie wydaje je indywidualnie. Możesz skontaktować się z nim, aby uzyskać jego procedurę. –