ATP

Improve factorizing

Registered by Tomer L

Currently all factors are being parsed. Factor only positive clauses, literals that are being resolved upon (need to change mechanism completely), check chapter on hyper resolution. Integrate factoring into resolution (currently are done in the deduction engine).

Blueprint information

Status:
Not started
Approver:
None
Priority:
Undefined
Drafter:
None
Direction:
Needs approval
Assignee:
Tomer L
Definition:
Approved
Series goal:
None
Implementation:
Unknown
Milestone target:
None

Related branches

Sprints

Whiteboard

(?)

Work Items

This blueprint contains Public information 
Everyone can see this information.

Subscribers

No subscribers.