| 2014 | Models for Logics and Conditional Constraints in Automated Proofs of Termination. | Salvador Lucas, Jos Meseguer |
| 2014 | Using Representation Theorems for Proving Polynomials Non-negative. | Salvador Lucas |
| 2014 | From Declarative Set Constraint Models to "Good" SAT Instances. | Frdric Lardeux, ric Monfroy |
| 2014 | Multivalued Elementary Functions in Computer-Algebra Systems. | David J. Jeffrey |
| 2014 | A Mathematical Hierarchy of Sudoku Puzzles and Its Computation by Boolean Grbner Bases. | Shutaro Inoue, Yosuke Sato |
| 2014 | A Rule-Based Expert System for Vaginal Cytology Diagnosis. | Carlos Gamallo-Chicano, Eugenio Roanes-Lozano, Carlos Gamallo-Amat |
| 2014 | A Distance-Based Decision in the Credal Level. | Amira Essaid, Arnaud Martin, Grgory Smits, Boutheina Ben Yaghlane |
| 2014 | Conformant Planning as a Case Study of Incremental QBF Solving. | Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler |
| 2014 | A Direct Propagation Method in Singly Connected Causal Belief Networks with Conditional Distributions for all Causes. | Oumaima Boussarsar, Imen Boukhris, Zied Elouedi |
| 2014 | Decomposition of Some Jacobian Varieties of Dimension 3. | Lubjana Beshaj, Tony Shaska |
| 2014 | Dynamic Symmetry Breaking in Itemset Mining. | Belad Benhamou |
| 2014 | Obtaining an ACL2 Specification from an Isabelle/HOL Theory. | Jess Aransay-Azofra, Jose Divasn, Jnathan Heras, Laureano Lambn, Mara Vico Pascual, ngel Luis Rubio, Julio Rubio |
| 2012 | Speeding Up Cylindrical Algebraic Decomposition by Grbner Bases. | David J. Wilson, Russell J. Bradford, James H. Davenport |
| 2012 | An Essence of SSReflect. | Iain Whiteside, David Aspinall, Gudmund Grov |
| 2012 | Isabelle/jEdit - A Prover IDE within the PIDE Framework. | Makarius Wenzel |
| 2012 | Point-and-Write - Documenting Formal Mathematics by Reference. | Carst Tankink, Christoph Lange, Josef Urban |
| 2012 | Abramowitz and Stegun - A Resource for Mathematical Document Analysis. | Alan P. Sexton |
| 2012 | A Combinator Language for Theorem Discovery. | Phil Scott, Jacques D. Fleuriot |
| 2012 | A System for Axiomatic Programming. | Gabriel Dos Reis |
| 2012 | A Query Language for Formal Mathematical Libraries. | Florian Rabe |
| 2012 | Real Algebraic Strategies for MetiTarski Proofs. | Grant Olney Passmore, Lawrence C. Paulson, Leonardo Mendona de Moura |
| 2012 | CDCL-Based Abstract State Transition System for Coherent Logic. | Mladen Nikolic, Predrag Janicic |
| 2012 | Writing on Clouds. | Vadim Mazalov, Stephen M. Watt |
| 2012 | Towards Understanding Triangle Construction Problems. | Vesna Marinkovic, Predrag Janicic |
| 2012 | Formalizing Frankl's Conjecture: FC-Families. | Filip Maric, Miodrag V. Zivkovic, Bojan Vuckovic |