Ricardo Caferra - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 45 from 45

2020

Automated DeductionThierry Boy de la Tour, Ricardo Caferra, Nicola Olivetti, Nicolas Peltier, Camilla Schwind. In Pierre Marquis, Odile Papini, Henri Prade, editors, A Guided Tour of Artificial Intelligence Research: Volume II: AI Algorithms. pages 53-81, Springer, 2020. [doi]

2011

Linear Temporal Logic and Propositional Schemata, Back and ForthVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. time 2011: 80-87 [doi]

Decidability and Undecidability Results for Propositional SchemataVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. jair, 40:599-656, 2011. [doi]

2010

RegSTAB: A SAT Solver for Propositional SchemataVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. cade 2010: 309-315 [doi]

A Decidable Class of Nested Iterated SchemataVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. cade 2010: 293-308 [doi]

Complexity of the Satisfiability Problem for a Class of Propositional SchemataVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. LATA 2010: 58-69 [doi]

Simplified handling of iterated term schemataVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. AMAI, 58(3-4):155-183, 2010. [doi]

Perfect Discrimination Graphs: Indexing Terms with Integer ExponentsHicham Bensaid, Ricardo Caferra, Nicolas Peltier. cade 2010: 369-383 [doi]

::::I::::-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost CompletenessHicham Bensaid, Ricardo Caferra, Nicolas Peltier. AISC 2010: 19-33 [doi]

2009

A Schemata Calculus for Propositional LogicVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. tableaux 2009: 32-46 [doi]

Dei: A Theorem Prover for Terms with Integer ExponentsHicham Bensaid, Ricardo Caferra, Nicolas Peltier. cade 2009: 146-150 [doi]

2008

More Flexible Term Schematisations via Extended Primal GrammarsVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. isaim 2008: [doi]

Accepting/rejecting propositions from accepted/rejected propositions: A unifying overviewRicardo Caferra, Nicolas Peltier. ijis, 23(10):999-1020, 2008. [doi]

2007

Towards Systematic Analysis of Theorem Provers Search Spaces: First StepsHicham Bensaid, Ricardo Caferra, Nicolas Peltier. wollic 2007: 38-52 [doi]

2006

Rewriting term-graphs with priorityRicardo Caferra, Rachid Echahed, Nicolas Peltier. ppdp 2006: 109-120 [doi]

2000

Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical RealizationRicardo Caferra, Nicolas Peltier, François Puitg. adg 2001: 268-305 [doi]

The Connection Method, Constraints and Model BuildingRicardo Caferra, Nicolas Peltier. BIRTHDAY 2000: 67-84

Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite ModelsRicardo Caferra, Nicolas Peltier. JSC, 29(2):177-211, 2000.

1997

A New Technique for Verifying and Correcting Logic ProgramsRicardo Caferra, Nicolas Peltier. JAR, 19(3):277-318, 1997.

1996

Review of Witold Marciszewski and Roman Murawski: Mechanization of Reasoning in a Historical PerspectiveRicardo Caferra. jancl, 6(3):287-288, 1996.

A Significant Extension of Logic Programming by Adapting Model Building RulesRicardo Caferra, Nicolas Peltier. elp 1996: 51-65

1995

A Generic Graphic Framework for Combining Inference Tools and Editing Proofs and FormulaeRicardo Caferra, Michel Herment. JSC, 19(1-3):217-243, 1995.

Extending Semantic Resolution via Automated Model Building: ApplicationsRicardo Caferra, Nicolas Peltier. IJCAI 1995: 328-334

Model Building and Interactive Theory DiscoveryRicardo Caferra, Nicolas Peltier. tableaux 1995: 154-168

Decision Procedures Using Model Building TechniquesRicardo Caferra, Nicolas Peltier. csl 1996: 130-144

1994

A Method for Building Models Automatically. Experiments with an Extension of OTTERChristophe Bourely, Ricardo Caferra, Nicolas Peltier. cade 1994: 72-86

1993

GLEFATINF: A Graphic Framework for Combining Theorem Provers and Editing Proofs for Different LogicsRicardo Caferra, Michel Herment. disco 1993: 229-240

A Tableaux Method for Systematic Simultaneous Search for Refutationas and Models Using Equational ProblemsRicardo Caferra. logcom, 3(1):3-25, 1993.

Cooperation between Direct Method and Translation Method in Non Classical Logics: Some Results in Propositional S5Ricardo Caferra, Stéphane Demri. IJCAI 1993: 74-79

A framework for the transfer of proofs, lemmas and strategies from classical to non classical logicsRicardo Caferra, Stéphane Demri, Michel Herment. sLogica, 52(2):197-232, 1993.

1992

A Method for Simultanous Search for Refutations and Models by Equational Constraint SolvingRicardo Caferra, Nicolas Zabel. JSC, 13(6):613-642, 1992.

Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical LogicRicardo Caferra, Stéphane Demri. cade 1992: 385-399

1991

User-oriented theorem proving with the ATINF graphic proof editorRicardo Caferra, Michel Herment, Nicolas Zabel. fair 1991: 2-10

Logic Morphisms as a Framework for Backward Transfer of Lemmas and Strategies in Some Modal and Epistemic LogicsRicardo Caferra, Stéphane Demri, Michel Herment. AAAI 1991: 421-426

1990

Extending Resolution for Model ConstructionRicardo Caferra, Nicolas Zabel. jelia 1991: 153-169

An Application of Many-Valued Logic to Decide Propositional S5 Formulae: A Strategy Designed for a Parameterized Tableaux-Based Theorem ProverRicardo Caferra, Nicolas Zabel. aimsa 1990: 23-32

1988

Some Tools for an Inference Laboratory (ATINF)Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade. cade 1988: 744-745

A Formal Approach to some Usually Informal Techniques Used in Mathematical ReasoningThierry Boy de la Tour, Ricardo Caferra. issac 1989: 402-406

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

1987

Proof Analogy in Interactive Theorem Proving: A Method to Express and Use It via Second Order Pattern MatchingThierry Boy de la Tour, Ricardo Caferra. AAAI 1987: 95-99

1985

Unification in Parallel with Refined Linearity Test: An Example of Recursive Network Structure in FP2, A Functional Parallel Programming LanguageRicardo Caferra, Philippe Jorrand. eurocal 1985: 539-540

1984

Program Synthesis Through Problem Splitting: A Method for Subproblem CharacterizationRamon Brena, Ricardo Caferra, Bertram Fronhöfer, Christian Gresse, Philippe Jacquet, Marie-Laure Potet. aimsa 1984: 113-120

Improvement of Recursive Programs from a Logic Programming Point of ViewBertram Fronhöfer, Ricardo Caferra, Philippe Jacquet. ki 1985: 229-237

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. PhD thesis, Joseph Fourier University, Grenoble, France, 1982. [doi]

Proof by Matrix Reduction as Plan + ValidationRicardo Caferra. cade 1982: 309-325

Sign in or sign up to see more results.

runs on WebDSL