Proof by Matrix Reduction as Plan + Validation. - Ricardo Caferra (CADE, 1982)

Abstraction, partage de structure et retour arrière non aveugle dans la méthode de réduction matricielle en démonstration automatique de théorèmes. (Abstraction, sharing of structure, and non-blind back to acking in the matrix reduction method in the automatic demonstration of theorems). - Ricardo Caferra (1982)

Program Synthesis Through Problem Splitting: A Method for Subproblem Characterization. - Ramon Brena; Ricardo Caferra; Bertram Fronhöfer; Christian Gresse; Philippe Jacquet; Marie-Laure Potet (AIMSA, 1984)

Improvement of Recursive Programs from a Logic Programming Point of View. - Bertram Fronhöfer; Ricardo Caferra; Philippe Jacquet (GWAI, 1984)

Unification in Parallel with Refined Linearity Test: An Example of Recursive Network Structure in FP2, A Functional Parallel Programming Language. - Ricardo Caferra; Philippe Jorrand (European Conference on Computer Algebra (2), 1985)

Proof Analogy in Interactive Theorem Proving: A Method to Express and Use It via Second Order Pattern Matching. - Thierry Boy de la Tour; Ricardo Caferra (AAAI, 1987)

A Formal Approach to some Usually Informal Techniques Used in Mathematical Reasoning. - Thierry Boy de la Tour; Ricardo Caferra (ISSAC, 1988)

Some Tools for an Inference Laboratory (ATINF). - Thierry Boy de la Tour; Ricardo Caferra; Gilles Chaminade (STACS, 1988)

An Application of Many-Valued Logic to Decide Propositional S5 Formulae: A Strategy Designed for a Parameterized Tableaux-Based Theorem Prover. - Ricardo Caferra; Nicolas Zabel (AIMSA, 1990)

Extending Resolution for Model Construction. - Ricardo Caferra; Nicolas Zabel (JELIA, 1990)

Logic Morphisms as a Framework for Backward Transfer of Lemmas and Strategies in Some Modal and Epistemic Logics. - Ricardo Caferra; Stéphane Demri; Michel Herment (AAAI, 1991)

User-oriented theorem proving with the ATINF graphic proof editor. - Ricardo Caferra; Michel Herment; Nicolas Zabel (FAIR, 1991)

Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic. - Ricardo Caferra; Stéphane Demri (CADE, 1992)

A Method for Simultanous Search for Refutations and Models by Equational Constraint Solving. - Ricardo Caferra; Nicolas Zabel (J. Symb. Comput., 1992)

GLEFATINF: A Graphic Framework for Combining Theorem Provers and Editing Proofs for Different Logics. - Ricardo Caferra; Michel Herment (DISCO, 1993)

Cooperation between Direct Method and Translation Method in Non Classical Logics: Some Results in Propositional S5. - Ricardo Caferra; Stéphane Demri (IJCAI, 1993)

A Tableaux Method for Systematic Simultaneous Search for Refutationas and Models Using Equational Problems. - Ricardo Caferra (J. Log. Comput., 1993)

A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics. - Ricardo Caferra; Stéphane Demri; Michel Herment (Stud Logica, 1993)

A Method for Building Models Automatically. Experiments with an Extension of OTTER. - Christophe Bourely; Ricardo Caferra; Nicolas Peltier (CADE, 1994)

Decision Procedures Using Model Building Techniques. - Ricardo Caferra; Nicolas Peltier (CSL, 1995)

Extending Semantic Resolution via Automated Model Building: Applications. - Ricardo Caferra; Nicolas Peltier (IJCAI, 1995)

Model Building and Interactive Theory Discovery. - Ricardo Caferra; Nicolas Peltier (TABLEAUX, 1995)

A Generic Graphic Framework for Combining Inference Tools and Editing Proofs and Formulae. - Ricardo Caferra; Michel Herment (J. Symb. Comput., 1995)

A Significant Extension of Logic Programming by Adapting Model Building Rules. - Ricardo Caferra; Nicolas Peltier (ELP, 1996)

Review of Witold Marciszewski and Roman Murawski: Mechanization of Reasoning in a Historical Perspective. - Ricardo Caferra (J. Appl. Non Class. Logics, 1996)

A New Technique for Verifying and Correcting Logic Programs. - Ricardo Caferra; Nicolas Peltier (J. Autom. Reason., 1997)

Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization. - Ricardo Caferra; Nicolas Peltier; François Puitg (Automated Deduction in Geometry, 2000)

The Connection Method, Constraints and Model Building. - Ricardo Caferra; Nicolas Peltier (Intellectics and Computational Logic, 2000)

Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite Models. - Ricardo Caferra; Nicolas Peltier (J. Symb. Comput., 2000)

Rewriting term-graphs with priority. - Ricardo Caferra; Rachid Echahed; Nicolas Peltier (PPDP, 2006)

Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps. - Hicham Bensaid; Ricardo Caferra; Nicolas Peltier (WoLLIC, 2007)

More Flexible Term Schematisations via Extended Primal Grammars. - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (ISAIM, 2008)

Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview. - Ricardo Caferra; Nicolas Peltier (Int. J. Intell. Syst., 2008)

Dei: A Theorem Prover for Terms with Integer Exponents. - Hicham Bensaid; Ricardo Caferra; Nicolas Peltier (CADE, 2009)

A Schemata Calculus for Propositional Logic. - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (TABLEAUX, 2009)

I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness. - Hicham Bensaid; Ricardo Caferra; Nicolas Peltier (AISC/MKM/Calculemus, 2010)

A Decidable Class of Nested Iterated Schemata. - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (IJCAR, 2010)

RegSTAB: A SAT Solver for Propositional Schemata. - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (IJCAR, 2010)

Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. - Hicham Bensaid; Ricardo Caferra; Nicolas Peltier (IJCAR, 2010)

Complexity of the Satisfiability Problem for a Class of Propositional Schemata. - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (LATA, 2010)

Simplified handling of iterated term schemata. - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (Ann. Math. Artif. Intell., 2010)

A Decidable Class of Nested Iterated Schemata (extended version) - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (CoRR, 2010)

Linear Temporal Logic and Propositional Schemata, Back and Forth. - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (TIME, 2011)

Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version) - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (CoRR, 2011)

Decidability and Undecidability Results for Propositional Schemata. - Vincent Aravantinos; Ricardo Caferra; Nicolas Peltier (J. Artif. Intell. Res., 2011)

Automated Deduction. - Thierry Boy de la Tour; Ricardo Caferra; Nicola Olivetti; Nicolas Peltier; Camilla Schwind (A Guided Tour of Artificial Intelligence Research (2) (II), 2020)