Soovitusi Otteri otsingu suunamiseks: erinevus redaktsioonide vahel
Mine navigeerimisribale
Mine otsikasti
Uus lehekülg: '= Meetodid keerulise tõestuse leidmiseks = == Põhistrateegia valik == * hyperres ilma goal-directed searchita, kui on horni lähedased reeglid: set(hyper_res). * binary res ...' |
Resümee puudub |
||
| (ei näidata sama kasutaja 2 vahepealset redaktsiooni) | |||
| 1. rida: | 1. rida: | ||
== Põhistrateegia valik == | == Põhistrateegia valik == | ||
| 13. rida: | 11. rida: | ||
set(factor). | set(factor). | ||
== Given ratio valik == | == Given ratio valik == | ||
| 33. rida: | 28. rida: | ||
== Splittimine == | == Splittimine == | ||
Vaatame, kas saab ülesande splittida alamülesanneteks a la | Vaatame, kas saab ülesande splittida alamülesanneteks a la p(a) | p(b) | ||
Siis teeme kaks eraldi tõestuseotsingut p(a) ja p(b) jaoks. | |||
== Võrduse orienteerimine == | == Võrduse orienteerimine == | ||
Viimane redaktsioon: 11. aprill 2013, kell 20:05
Põhistrateegia valik
- hyperres ilma goal-directed searchita, kui on horni lähedased reeglid: set(hyper_res).
- binary res koos goal-directed searchiga (kasuta sos ja usable): set(binary_res).
- binary res ilma goal-directed searchita, aga lisapiirangutega: set(binary_res) ja vaata lisaks.
- üks eeldus peab olema unit
- mingi spetsiifiline literaalide järjestus, kus tohib kasutada ainult järjestuse mõttes suuremaid disjunkte
Alati ka:
set(factor).
Given ratio valik
- N korda vali kõige väiksem disjunkt
- 1 kord vali queuest
Enamasti on mõistlik panna ratio ca 4: assign(pick_given_ratio,4).
Piirangud järeldatavatele disjunktidele
- piirame ära sügavuse (saab teha weight templatede abil).
- piirame ära literaalide arvu disjunktis, a la assign(max_literals,3).
- piirame ära disjunkti elementide koguarvu (weight), a la assign(max_weight,13).
Splittimine
Vaatame, kas saab ülesande splittida alamülesanneteks a la p(a) | p(b)
Siis teeme kaks eraldi tõestuseotsingut p(a) ja p(b) jaoks.
Võrduse orienteerimine
Võrduse juures on võimalik määrata, kuidas orienteeritakse võrdusi (otteril lex parameeter) a la kas orienteerida f(x)=g(x)
- f(x)->g(x) või
- g(x)->f(x)