I want to encode a ruleset for a domain in first-order predicate logic.
Next, I want the computer to "reason" about this ruleset. By "reason" I
mean: discover rule invariants, decompose functions (i.e., break up
conjunctions/disjunctions), perform goal regression, etc.
Is Prolog the right tool for this job? Can I express such rulesets
naturally in Prolog? Can Prolog push those symbols around without extra
help? Contrast with C, where I'd have to write my own
parser/interpreter/resolution engine/etc. for FOPL.
If not Prolog, what is the right tool for the job?