predicate-logic
Strategie rozwiązywania zadań z logiki predykatów dla matematyków i logików
Instalacja
Wybierz klienta i sklonuj repozytorium do odpowiedniego katalogu skilli.
Instalacja
O skillu
Umiejętność Claude'a do pracy z problemami logiki predykatów w logice matematycznej. Zawiera narzędzia do analizy kwantyfikatorów, konwersji do postaci preneksowej, skolemizacji i budowania dowodów rezolucyjnych. Pozwala na weryfikację formuł logicznych, konstruowanie modeli kontrprzykładów i automatyczne sprawdzanie poprawności argumentów logicznych za pomocą solvera Z3.
Jak używać
Zainstaluj umiejętność w swoim środowisku Claude'a, umieszczając folder predicate-logic w katalogu .claude/skills/math/mathematical-logic/ projektu.
Zidentyfikuj typ problemu logiki predykatów, który chcesz rozwiązać: czy wymaga analizy kwantyfikatorów (uniwersalnych ForAll lub egzystencjalnych Exists), konwersji do postaci normalnej, czy budowy dowodu.
Dla problemów z kwantyfikatorami uniwersalnymi użyj komendy z3_solve.py prove z formułą zawierającą ForAll, aby zweryfikować, czy dana formuła jest tautologią lub wynika logicznie z przesłanek.
Dla problemów z kwantyfikatorami egzystencjalnymi zastosuj skolemizację, zamieniając kwantyfikatory egzystencjalne na funkcje Skolema, a następnie użyj solvera do sprawdzenia spełnialności formuły.
Jeśli chcesz obalić argument logiczny, skonstruuj kontrmodel za pomocą komendy z3_solve.py model, która znajdzie interpretację, w której przesłanki są prawdziwe, ale konkluzja fałszywa.
Dla złożonych dowodów przeprowadź rezolucję: przekonwertuj formułę do postaci normalnej koniunkcyjnej (CNF), zaneguj konkluzję i stosuj regułę rezolucji aż do uzyskania klauzuli pustej (dowód) lub nasycenia (brak dowodu).