Filtrer vos résultats
- 17
- 12
- 3
- 1
- 1
- 17
- 3
- 3
- 3
- 2
- 3
- 3
- 17
- 16
- 15
- 15
- 1
- 1
- 1
- 1
- 1
- 17
- 9
- 6
- 4
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
17 résultats
|
|
|
triés par
|
|
|
Alethe: Towards a Generic SMT Proof Format (extended abstract)PxTP 2021 - 7th Workshop on Proof eXchange for Theorem Proving, Sep 2021, Pittsburgh, PA / virtual, United States. pp.49-54, ⟨10.4204/EPTCS.336.6⟩
Communication dans un congrès
hal-03341413v1
|
||
|
|
A Verified SAT Solver Framework with Learn, Forget, Restart, and IncrementalityIJCAI 2017 - 26th International Joint Conference on Artificial Intelligence, Aug 2017, Melbourne, Australia. pp.4786-4790, ⟨10.24963/ijcai.2017/667⟩
Communication dans un congrès
hal-01592164v1
|
||
|
|
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality8th International Joint Conference on Automated Reasoning (IJCAR 2016), Jun 2016, Coimbra, Portugal. ⟨10.1007/978-3-319-40229-1_4⟩
Communication dans un congrès
hal-01336074v1
|
||
|
|
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOLFSCD 2017: 2nd International Conference on Formal Structures for Computation and Deduction, Sep 2017, Oxford, United Kingdom. pp.1 - 11, ⟨10.4230/LIPIcs.FSCD.2017.11⟩
Communication dans un congrès
hal-01599176v1
|
||
|
|
Reconstructing veriT Proofs in Isabelle/HOLPxTP 2019 - Sixth Workshop on Proof eXchange for Theorem Proving, Aug 2019, Natal, Brazil. pp.36-50, ⟨10.4204/EPTCS.301.6⟩
Communication dans un congrès
hal-02276530v1
|
||
|
|
PxTP 2021 - Seventh Workshop on Proof eXchange for Theorem ProvingElectronic Proceedings in Theoretical Computer Science, 336, 61 p., 2021, ⟨10.4204/eptcs.336⟩
N°spécial de revue/special issue
hal-03443742v1
|
||
|
|
Semi-intelligible Isar Proofs from Machine-Generated ProofsJournal of Automated Reasoning, 2016, ⟨10.1007/s10817-015-9335-3⟩
Article dans une revue
hal-01211748v1
|
||
|
|
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Extended Abstract)Isabelle Workshop 2016, Aug 2016, Nancy, France
Communication dans un congrès
hal-01401807v1
|
||
|
|
Foundational (Co)datatypes and (Co)recursion for Higher-Order LogicFrontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. pp.3-21, ⟨10.1007/978-3-319-66167-4_1⟩
Communication dans un congrès
hal-01592196v1
|
||
|
|
SPASS-SATT: A CDCL(LA) SolverCADE-27 - The 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. pp.111-122, ⟨10.1007/978-3-030-29436-6_7⟩
Communication dans un congrès
hal-02405524v1
|
||
|
|
Better SMT Proofs for Easier ReconstructionAITP 2019 - 4th Conference on Artificial Intelligence and Theorem Proving, Apr 2019, Obergurgl, Austria
Communication dans un congrès
hal-02381819v1
|
||
|
|
A Verified SAT Solver Framework with Learn, Forget, Restart, and IncrementalityJournal of Automated Reasoning, 2018, 61 (1-4), pp.333-365. ⟨10.1007/s10817-018-9455-7⟩
Article dans une revue
hal-01904579v1
|
||
|
|
Scalable Fine-Grained Proofs for Formula ProcessingJournal of Automated Reasoning, 2020, 64 (3), pp.485-510. ⟨10.1007/s10817-018-09502-y⟩
Article dans une revue
hal-02515103v1
|
||
|
|
A verified SAT solver with watched literals using imperative HOLCPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. ⟨10.1145/3167080⟩
Communication dans un congrès
hal-01904647v1
|
||
|
|
A Verified SAT Solver Framework including Optimization and Partial ValuationsLPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2020, Alicante, Spain. pp.212-193, ⟨10.29007/96wb⟩
Communication dans un congrès
hal-02963986v1
|
||
|
|
Reliable Reconstruction of Fine-Grained Proofs in a Proof AssistantCADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. ⟨10.1007/978-3-030-79876-5⟩
Communication dans un congrès
hal-03341357v1
|
||
|
|
Formalization of Logical Calculi in Isabelle/HOLLogic in Computer Science [cs.LO]. Universität des Saarlandes Saarbrücken, 2020. English. ⟨NNT : ⟩
Thèse
tel-02963301v1
|