[![Hackathon Banner](https://hackmd.io/_uploads/r1YSBHv1kl.png)](https://hackmd.io/@TP6ad1ylQI6J_evTjOJmeg/ryrJNvQ0A) # What You'll Be Building As a participant, you'll be submitting two pieces of work: 1. [a Logic Program Insurance Contract encoding (or multiple) that can be integrated into the CodeX Insurance Analyst (CIA) system](#Logic-Program-Insurance-Contract-encoding-for-CIA), and 2. [Evidence of Correctness](#Evidence-of-Correctness) demonstrating that your encoding(s) correctly represent(s) the coverage expressed in your insurance policy (or policies) of choice. **We strongly recommend reading the rest of this page.** You'll find details as to what and how you'll be submitting during the event. ## How will you submit? You will submit your Logic Program Insurance Contract encoding by uploading it to a sandbox version of the CIA system. You will submit your Evidence of Correctness by making a post in the [Submissions channel on the Discord](https://discord.com/channels/1290059547209109636/1294474827788455946) containing: 1. the names of everyone on your team, 2. your username(s) on the CIA sandbox, and 3. a link to a GitHub repo containing any files that comprise the Evidence of Correctness. ## What policies can you encode? **Short answer:** Any insurance policy of your choice, but we recommend encoding the policies we provide. **Long answer:** On the day of the event, we (CodeX) will provide a list of insurance policies that are of particular interest to us, that we are familiar with, and that we think are particularly well-suited to being encoded as logic programs. We recommend that you encode coverage from those policies, at least for this event. But if you have an insurance policy that you would rather encode, you are welcome to do so! If you do, you will need to provide us with the policy text and its source, and it may be more difficult for us to confirm the correctness of your encoding. Tip: Our method of encoding contracts is best suited to personal lines insurance policies, especially those that are non-bespoke. ## Logic Program Insurance Contract encoding for CIA :::warning This section assumes the reader has a basic knowledge of logic programming, either in Prolog or Epilog. The examples will be presented in Epilog, the logic programming language used in the [Stanford course on logic programming](http://logicprogramming.stanford.edu/public/index.php). Epilog as it is used in Logic Program Insurance Contracts is extremely similar to Prolog, but with some syntactic differences, and without cut and assert/retract. And, unlike Prolog, Epilog makes a formal distinction between rules and data. ::: There are many possible structures for Logic Program Insurance Contracts. Generally, the following is true: * The dataset represents the *information about the world and an insurance claim* that is relevant for determining whether a certain situation (described by facts pertaining to the claim) would be covered by an insurance policy. * The ruleset represents the *terms and conditions of an insurance policy* that are relevant to determining whether a situation is covered by the policy. * The ruleset defines a relation `covers` such that `covers` holds of a claim object iff the insurance policy would cover the situation described by the facts in the dataset pertaining to the claim. The Logic Program Insurance Contracts deployed on the CodeX Insurance Analyst platform need to meet a few additional constraints. These constraints are nontrivial, but we have found that they do not place excessive limits on expressiveness. Such contracts must: * **Be written in Epilog.** * The current system uses an Epilog interpreter. * **Encode coverage for single benefits, not entire policies.** * Insurance coverage is usually divided into multiple benefits, which cover different (though potentially overlapping) situations. On the current CIA platform, each Logic Program Insurance Contract encodes coverage for a single benefit. * For example, a life insurance policy might have a "Death Benefit" that pays when the insured person dies, and a "Terminal Illness Benefit" that pays when the insured person is diagnosed as terminally ill. On the current CIA platform, these benefits would be encoded as distinct Logic Program Insurance Contracts. * Note: During the event, you are welcome to encode coverage for multiple benefits. They will just need to be submitted to the CIA system as distinct Logic Program Insurance Contracts. * **Define a binary `covers` relation in the ruleset.** Specifically, such that `covers(P, C)` holds of a policy `P` and a claim `C` iff the `policy.type` of `P` corresponds to the benefit whose coverage is encoded in the ruleset, and that benefit would cover the situation described by `C`. * Note that this doesn't concern the *quantity of payout* by the policy, only whether the policy covers the claim at all. * **Obey the following contraints on base relations:** * Policy objects can only have the following attributes (but don't need all of them): * `type`, which corresponds to the benefit of the policy you're encoding. * `insuree`, which is the person insured by the policy. * `startdate` and `enddate`, which correspond to the start date and end date of the policy's coverage, respectively. * Information that varies between claims is represented using attribute relations. (I.e. binary relations in which the first argument is a claim object.) * Person objects can only have the following attributes (but don't need all of them): `gender`, `dob` (i.e. date of birth), `parent`, `nationality`, and `residence` (i.e. country of residence). * Functional terms cannot have functional terms as arguments. * **Store in the "world" dataset those facts which (i) are relevant to determining coverage, (ii) don't vary based on the claim, and (iii) aren't claim attributes.** The "world" dataset is merged with the claim dataset before determining coverage for a given claim. Each Logic Program Insurance Contract in CIA defines its own "world" dataset. * For example, if coverage for an auto accident claim depends on the continent in which the accident occurred, you might define a binary `continent_of` relation in the dataset, such that `continent_of(C1, C2)` holds iff the country `C1` is the continent `C2`. * **Provide a metadata file which explicitly lists all of the claim attributes the program uses.** * For example, consider a Logic Program Insurance Contract which defines coverage for policies of type `insurance_benefit_1`. It expects claim datasets to have the attributes `claim.date` and `claim.claimant`. Then its metadata file should contain the lines `attribute(insurance_benefit_1, claim.date)` and `attribute(insurance_benefit_1, claim.claimant)`. [//]: # (Though the above are minimum requirements for a Logic Program Insurance Contract that can be deployed on CIA, there is additional information you can provide that will better integrate your encoding into the system.) ### Example Consider a hypothetical insurance policy that has two benefits. The first, Benefit A, provides coverage for the insured if the claim is filed for an accident that occured in North America. The second, Benefit B, does the same for an accident that occurred in Africa. A logic program encoding for Benefit A might look like the following ruleset: ``` covers(P, C) :- policy.type(P, benefit_a) & policy.insuree(P, Insuree) & claim.claimant(C, Insuree) & claim.accident_occurred_in_country(C, Country) & continent_of(Country, north_america) ``` The following "world" dataset: ``` continent_of(afghanistan, asia) ... continent_of(zimbabwe, africa) ``` And the following metadata: ``` attribute(benefit_a, claim.claimant) attribute(benefit_a, claim.accident_occurred_in_country) ``` Note that this contract is (a) written in Epilog, (b) encodes the coverage for a single benefit of the policy, \(c\) defines an appropriate binary `covers` relation, (d) obeys the constraints on the base relations, (e) stores the appropriate facts in the "world" dataset, and (f) provides a metadata file that explicitly lists all of the claim attributes used in the encoding. </code> ## Evidence of Correctness An important part of developing a useful computable contract is being able to demonstrate its correctness. That is, being able to demonstrate that the computable contract faithfully represents the terms and conditions of the contract or policy being encoded. **In the context of Logic Program Insurance Contracts,** this means providing evidence that, when evaluated on a dataset containing all information relevant to determining whether an insurance claim is covered under the policy, the logic program rules will correctly determine whether the claim should be covered by the policy. ### What does Evidence of Correctness look like? > "One can't proceed from the informal to the formal by formal means." > &nbsp;&nbsp;&nbsp;&nbsp; -Alan Perlis We aren't asking for *proof* of correctness. Though insurance policies are particularly amenable to being represented in a rigorous, logical manner, we understand that they're written in less-than-perfectly-precise natural language. As such, you will not be able to provide unambiguous, mathematical proof of the correctness of your encoding. Instead, the Evidence of Correctness is meant to convince other people *with access to your encoding and the original policy wording* that your encoding is correct. There are many possible ways to do this, and you are encouraged to be as creative as you want in your approach to this portion of the submission! That said, if you want some guidance, here are some actionable tips for making your Evidence of Correctness: * **When encoding your policy, you may have to make a judgment call as to how to interpret policy wording. When this occurs, document your decision!** * Even if you're ultimately wrong, it is helpful to explain the different interpretations you considered and why and how you chose the interpretation you did. (At an insurance company, a person encoding a policy can potentially speak to the policy author, a claims adjudicator, or an insurance lawyer to understand how to interpret a portion of a policy. We unfortunately don't have that luxury during this event, so documenting decisions and uncertainty is vital!) * **High-level Example:** Insurance policies will often define a term and provide a list of examples of that term. Depending on the context, that list of examples may or may not be exhaustive, and whether it is exhaustive will rarely be explicitly stated. You will likely have to choose whether to interpret that list as exhaustive. * **Document your process.** * Explain how you approached developing the encoding and understanding the policy wording. How did you determine which portions of the policy wording were relevant to coverage for a specific benefit? How did you determine which portions weren't relevant? If you had to reference documents other than the policy wording, how did you determine what those were? How did you decide the relevant portions of those documents? If you didn't understand a portion of a document you needed to encode, what did you do? * **Cite relevant portions of the policy and other documents.** * Let us know what portions of the policy and other documents you encoded, and which portions of your encoding correspond to which parts of the encoded documents. * **Explain the structure of the policy wording.** * Help us to understand the structure of the coverage in the policy by explaining the policy wording at a high level. * **Explain the structure of your encoding.** * Help us understand how your encoding works by explaining the structure of your logic program ruleset. * **Provide affirmative and negative examples.** * You're likely unit testing your encoding by testing your contract on datasets corresponding to claims that you expect to be covered/not covered by the policy you're encoding. You could provide these examples and explanations/descriptions of them as part of your Evidence of Correctness. * **Demonstrate that you didn't miss any exclusions.** * Because of how insurance policies are structured, wording from any portion of the policy has the potential to be relevant to coverage in any benefit. You'll want to demonstrate that you didn't miss any relevant portions of the policy wording. (For example, some homeowners' policies will provide coverage for water damage, and express exclusions to that coverage >100 pages later.) ## Evaluation Criteria Judging of submissions will take into account the following: * **Complexity of the encoded insurance coverage.** * **Correctness of the encoding.** * **Scope of the encoded coverage.** * **Readability of the logic program.** * **Usability of the logic program by the end user.** * **Evidence of Correctness:** * **Efficacy** (i.e. ability to demonstrate correctness) * **Exhaustiveness** of the encoding that it provides evidence for. * **Relevance** of the evidence to the encoding it provides evidence for. ## FAQs Will be posted here as they are asked! ## Have questions? If you can't find the answer on this site, feel free to reach out to [Preston Carlson](mailto:pjames27@stanford.edu), the Computable Contracts Developer at CodeX.