equal
deleted
inserted
replaced
5 |
5 |
6 Proofs trace the inferences of the solver. They can be used to check unsatisfiability results. |
6 Proofs trace the inferences of the solver. They can be used to check unsatisfiability results. |
7 |
7 |
8 The proof language is inspired by: |
8 The proof language is inspired by: |
9 |
9 |
10 Leonardo de Moura and Nikolaj Bj/orner. Proofs and Refutations, and Z3. In |
10 Leonardo de Moura and Nikolaj Bjørner. Proofs and Refutations, and Z3. In |
11 Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof |
11 Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof |
12 Assistants, and the 7th International Workshop on the Implementation of Logics, |
12 Assistants, and the 7th International Workshop on the Implementation of Logics, |
13 volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. |
13 volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. |
14 *) |
14 *) |
15 |
15 |