LogicUS.PL.HornRS

The module provides the tools to work with Horn Reasoning Systems (HRS) through the definition of facts and rules and the use of forward and backward chaining to make deductions. Conversion to standard formulas and clauses is also provided to apply other algorithms on them.

HRS Elements

type alias HornFact =

PSymb

It defines a fact as a propositional variable. Use ("⟂", []) for represent inconsistence and ("⊤", []) for represent tautology.

type alias HornRule =

( Set HornFact, HornFact )

It defines an inference rule of Horn as a tuple whose first element regards to the antecedents of the rule and the second one to de consecuent of the rule.

type alias HornKB =

Set HornFact

It defines a Knowledge Base of Horn as a set of facts.

HRS Deductions I: Forward Chaining

type alias FwChRow =

{ step : Int

, kb : HornKB

, avRules : List Int

, shRules : List Int

, newFacts : HornKB

}

It defines a row of a table of FC process with the properties:

step: indicates the step of the algorithm
kb: indicates the knowledge base handled at the regarding step
avRules : indicates the indices of rules available at the regarding step
shRules : indicates the indices of rules shooted at the regarding step
newFacts : indicates the new knowledge deducted at the regarding step

type alias FwChResult =

{ rules : List HornRule

, initialKB : HornKB

, goal : HornFact

, table : List FwChRow

, res : Bool

}

It holds the result of forward chaining process including rules, the initial KB, the goal, a table that summarizes the development of the algorithm and the result (if the goal can be deducted from initial KB with the rules given )

forwardChaining1 : List HornRule -> HornKB -> HornFact -> FwChResult

It performs forwardChaining algorithm with removing, at each step, the rules shot from available rules.

forwardChaining2 : List HornRule -> HornKB -> HornFact -> FwChResult

It performs forwardChaining algorithm with removing, at each step, the rules whose consecuent is already in the KB from available rules.

forwardChainingResultToMDString : FwChResult -> String

It generates a markdown string (includinf latex notation) of the result of a forwarding chaining execution.

HRS Deductions II: Backward Chaining

type alias BwChRow =

{ step : Int

, opened : List ( Bool, HornKB )

, currentNode : Maybe HornKB

, goal : Maybe HornFact

, descendents : List ( Bool, Int, List ( Bool, HornFact ) )

}

It defines a row of a table of BW process with the properties:

step: indicates the step of the algorithm
opened: indicates the opened ways at the regarding step
currentNode : indicates the way treated at the regarding step
goal : indicates the goal of currentNode way treated at the regarding step
descendents : indicates the new ways deducted at the regarding step

type alias BwChResult =

{ rules : List HornRule

, initialKB : HornKB

, goal : HornFact

, table : List BwChRow

, res : Bool

}

It holds the result of backward chaining process including rules, the initial KB, the goal, a table that summarizes the development of the algorithm and the result (if the goal can be deducted from initial KB with the rules given).

backwardChaining1 : List HornRule -> HornKB -> HornFact -> BwChResult

It performs the backward chaining algorithm by selecting at each step the way with the fewest remaining goals and the goal using alphabetical order.

backwardChainingResultToMDString : BwChResult -> String

It generates a MD string (including latex notation) of the result of an execution of BC algorithm

HRS Trasformations

hornFactToFPL : HornFact -> FormulaPL

It transform a Horn fact to a standard formula

hornKBToSPL : HornKB -> SetPL

It transform a Horn KB to a standard formula set

hornRuleToFPL : HornRule -> FormulaPL

It transform a Horn rule to a standard formula

hornRulesToSPL : List HornRule -> SetPL

It transform a list of Horn rules to a standard formula

hornFactToClause : HornFact -> ClausePL

It transform a Horn fact to a clause

hornKBToClauses : HornKB -> ClausePLSet

It transform a Horn kb to a set of clauses

hornRuleToClause : HornRule -> ClausePL

It transform a Horn rule to a clause

hornRulesToClauses : List HornRule -> ClausePLSet

It transform a list of Horn rules to a set of clauses

HRS Parser

hornFactReadFromString : String -> ( Maybe HornFact, String, String )

It reads a Horn fact from a string. The string may correspond to:

A string of uppercase letters optionaly subindexed using "{" "}" as delimiters and integers separated by commas as indices. Ex: "P", "PAUL", "P{1}", "PAUL_{1,2,3}"
A string with "!F" that represents inconsistence.
A string with "!T" that represents tautology.

It gives a tuple with the Horn fact (if it could be read) , the input string and the message of error (if fact couldn't be read).

hornFactReadExtraction : ( Maybe HornFact, String, String ) -> HornFact

It extract the Horn fact read. If it is not present it returns a fact of inconsistency

hornFactToInputString : HornFact -> String

It generates the string that corresponds to the input of a given Horn fact

hornKBReadFromString : String -> ( Maybe HornKB, String, String )

It reads a Horn KB from a string. The string has to match to a serial of facts separated by commas, following the rules defined for facts parsing.

It gives a tuple with the Horn KB (if it could be read) , the input string and the message of error (if fact couldn't be read).

hornKBReadExtraction : ( Maybe HornKB, String, String ) -> HornKB

It extract the Horn KB read. If it is not present it returns an empty set

hornKBToInputString : HornKB -> String

It generates the string that corresponds to the input of a given Horn KB

hornRuleReadFromString : String -> ( Maybe HornRule, String, String )

It reads a Horn rule from a string. The string has to match to a serial of facts separated by & for the antecedents, followed by the symbol -> and a unique fact as consecuent.

It gives a tuple with the Horn rule (if it could be read) , the input string and the message of error (if fact couldn't be read).

hornRuleReadExtraction : ( Maybe HornRule, String, String ) -> HornRule

It extract the Horn rule read. If it is not present it returns a rule with inconsistence as antecedent and consecuent

hornRuleToInputString : HornRule -> String

It generates the string that corresponds to the input of a given Horn rule

hornRulesReadFromString : String -> ( Maybe (List HornRule), String, String )

It reads a Horn rule list from a string. The string has to match to a serial of rules separated by commas.

It gives a tuple with the Horn rule list (if it could be read) , the input string and the message of error (if fact couldn't be read).

hornRulesReadExtraction : ( Maybe (List HornRule), String, String ) -> List HornRule

It extract the list of Horn rules read. If it is not present it returns an empty list

hornRulesToInputString : List HornRule -> String

It generates the string that corresponds to the input of a given list of Horn rules

HRS Representations

hornFactToString : HornFact -> String

It gives the string representation of a Horn fact using unicode notation

hornFactToMathString : HornFact -> String

It gives the string representation of a Horn fact using latex notation

hornKBToStringComma : HornKB -> String

It gives the string representation of a Horn KB separating facts by comma using unicode notation

hornKBToStringWedge : HornKB -> String

It gives the string representation of a Horn KB separating facts by & using unicode notation

hornKBToMathStringComma : HornKB -> String

It gives the string representation of a Horn KB separating facts by comma using latex notation

hornKBToMathStringWedge : HornKB -> String

It gives the string representation of a Horn KB separating facts by & using latex notation

hornRuleToString : HornRule -> String

It gives the string representation of a Horn rule using unicode notation

hornRuleToMathString : HornRule -> String

It gives the string representation of a Horn rule using latex notation

hornRulesToString : List HornRule -> String

It gives the string representation of a Horn rule list using unicode notation and indexing the formulas by its position in the list

hornRulesToMathString : List HornRule -> String

It gives the string representation of a Horn rule list using latex notation and indexing the formulas by its position in the list

logicUSLIB/logicus-pl/2.0.0