default search action
Ricardo Caferra
Person information
- affiliation: IMAG, Grenoble, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2020
- [p1]Thierry Boy de la Tour, Ricardo Caferra, Nicola Olivetti, Nicolas Peltier, Camilla Schwind:
Automated Deduction. A Guided Tour of Artificial Intelligence Research (2) (II) 2020: 53-81
2010 – 2019
- 2014
- [i3]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
Decidability and Undecidability Results for Propositional Schemata. CoRR abs/1401.3900 (2014) - 2011
- [j10]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
Decidability and Undecidability Results for Propositional Schemata. J. Artif. Intell. Res. 40: 599-656 (2011) - [c33]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
Linear Temporal Logic and Propositional Schemata, Back and Forth. TIME 2011: 80-87 - [i2]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version). CoRR abs/1102.2174 (2011) - 2010
- [j9]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
Simplified handling of iterated term schemata. Ann. Math. Artif. Intell. 58(3-4): 155-183 (2010) - [c32]Hicham Bensaid, Ricardo Caferra, Nicolas Peltier:
I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness. AISC/MKM/Calculemus 2010: 19-33 - [c31]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
A Decidable Class of Nested Iterated Schemata. IJCAR 2010: 293-308 - [c30]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
RegSTAB: A SAT Solver for Propositional Schemata. IJCAR 2010: 309-315 - [c29]Hicham Bensaid, Ricardo Caferra, Nicolas Peltier:
Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. IJCAR 2010: 369-383 - [c28]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
Complexity of the Satisfiability Problem for a Class of Propositional Schemata. LATA 2010: 58-69 - [i1]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
A Decidable Class of Nested Iterated Schemata (extended version). CoRR abs/1001.4251 (2010)
2000 – 2009
- 2009
- [c27]Hicham Bensaid, Ricardo Caferra, Nicolas Peltier:
Dei: A Theorem Prover for Terms with Integer Exponents. CADE 2009: 146-150 - [c26]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
A Schemata Calculus for Propositional Logic. TABLEAUX 2009: 32-46 - 2008
- [j8]Ricardo Caferra, Nicolas Peltier:
Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview. Int. J. Intell. Syst. 23(10): 999-1020 (2008) - [c25]Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier:
More Flexible Term Schematisations via Extended Primal Grammars. ISAIM 2008 - 2007
- [c24]Hicham Bensaid, Ricardo Caferra, Nicolas Peltier:
Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps. WoLLIC 2007: 38-52 - 2006
- [c23]Ricardo Caferra, Rachid Echahed, Nicolas Peltier:
Rewriting term-graphs with priority. PPDP 2006: 109-120 - 2000
- [j7]Ricardo Caferra, Nicolas Peltier:
Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite Models. J. Symb. Comput. 29(2): 177-211 (2000) - [c22]Ricardo Caferra, Nicolas Peltier, François Puitg:
Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization. Automated Deduction in Geometry 2000: 268-305 - [c21]Ricardo Caferra, Nicolas Peltier:
The Connection Method, Constraints and Model Building. Intellectics and Computational Logic 2000: 67-84 - [e1]Ricardo Caferra, Gernot Salzer
:
Automated Deduction in Classical and Non-Classical Logics, Selected Papers. Lecture Notes in Computer Science 1761, Springer 2000, ISBN 3-540-67190-0 [contents]
1990 – 1999
- 1997
- [j6]Ricardo Caferra, Nicolas Peltier:
A New Technique for Verifying and Correcting Logic Programs. J. Autom. Reason. 19(3): 277-318 (1997) - 1996
- [j5]Ricardo Caferra:
Review of Witold Marciszewski and Roman Murawski: Mechanization of Reasoning in a Historical Perspective. J. Appl. Non Class. Logics 6(3): 287-288 (1996) - [c20]Ricardo Caferra, Nicolas Peltier:
A Significant Extension of Logic Programming by Adapting Model Building Rules. ELP 1996: 51-65 - 1995
- [j4]Ricardo Caferra, Michel Herment:
A Generic Graphic Framework for Combining Inference Tools and Editing Proofs and Formulae. J. Symb. Comput. 19(1-3): 217-243 (1995) - [c19]Ricardo Caferra, Nicolas Peltier:
Decision Procedures Using Model Building Techniques. CSL 1995: 130-144 - [c18]Ricardo Caferra, Nicolas Peltier:
Extending Semantic Resolution via Automated Model Building: Applications. IJCAI 1995: 328-334 - [c17]Ricardo Caferra, Nicolas Peltier:
Model Building and Interactive Theory Discovery. TABLEAUX 1995: 154-168 - 1994
- [c16]Christophe Bourely, Ricardo Caferra, Nicolas Peltier:
A Method for Building Models Automatically. Experiments with an Extension of OTTER. CADE 1994: 72-86 - 1993
- [j3]Ricardo Caferra:
A Tableaux Method for Systematic Simultaneous Search for Refutationas and Models Using Equational Problems. J. Log. Comput. 3(1): 3-25 (1993) - [j2]Ricardo Caferra, Stéphane Demri, Michel Herment:
A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics. Stud Logica 52(2): 197-232 (1993) - [c15]Ricardo Caferra, Michel Herment:
GLEFATINF: A Graphic Framework for Combining Theorem Provers and Editing Proofs for Different Logics. DISCO 1993: 229-240 - [c14]Ricardo Caferra, Stéphane Demri:
Cooperation between Direct Method and Translation Method in Non Classical Logics: Some Results in Propositional S5. IJCAI 1993: 74-79 - 1992
- [j1]Ricardo Caferra, Nicolas Zabel:
A Method for Simultanous Search for Refutations and Models by Equational Constraint Solving. J. Symb. Comput. 13(6): 613-642 (1992) - [c13]Ricardo Caferra, Stéphane Demri:
Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic. CADE 1992: 385-399 - 1991
- [c12]Ricardo Caferra, Stéphane Demri, Michel Herment:
Logic Morphisms as a Framework for Backward Transfer of Lemmas and Strategies in Some Modal and Epistemic Logics. AAAI 1991: 421-426 - [c11]Ricardo Caferra, Michel Herment, Nicolas Zabel:
User-oriented theorem proving with the ATINF graphic proof editor. FAIR 1991: 2-10 - 1990
- [c10]Ricardo Caferra, Nicolas Zabel:
An Application of Many-Valued Logic to Decide Propositional S5 Formulae: A Strategy Designed for a Parameterized Tableaux-Based Theorem Prover. AIMSA 1990: 23-32 - [c9]Ricardo Caferra, Nicolas Zabel:
Extending Resolution for Model Construction. JELIA 1990: 153-169
1980 – 1989
- 1988
- [c8]Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade:
Some Tools for an Inference Laboratory (ATINF). CADE 1988: 744-745 - [c7]Thierry Boy de la Tour, Ricardo Caferra:
A Formal Approach to some Usually Informal Techniques Used in Mathematical Reasoning. ISSAC 1988: 402-406 - [c6]Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade:
Some Tools for an Inference Laboratory (ATINF). STACS 1988: 395-396 - 1987
- [c5]Thierry Boy de la Tour, Ricardo Caferra:
Proof Analogy in Interactive Theorem Proving: A Method to Express and Use It via Second Order Pattern Matching. AAAI 1987: 95-99 - 1985
- [c4]Ricardo Caferra, Philippe Jorrand:
Unification in Parallel with Refined Linearity Test: An Example of Recursive Network Structure in FP2, A Functional Parallel Programming Language. European Conference on Computer Algebra (2) 1985: 539-540 - 1984
- [c3]Ramon Brena, Ricardo Caferra, Bertram Fronhöfer, Christian Gresse, Philippe Jacquet, Marie-Laure Potet:
Program Synthesis Through Problem Splitting: A Method for Subproblem Characterization. AIMSA 1984: 113-120 - [c2]Bertram Fronhöfer, Ricardo Caferra, Philippe Jacquet:
Improvement of Recursive Programs from a Logic Programming Point of View. GWAI 1984: 229-237 - 1982
- [b1]Ricardo Caferra:
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). Joseph Fourier University, Grenoble, France, 1982 - [c1]Ricardo Caferra:
Proof by Matrix Reduction as Plan + Validation. CADE 1982: 309-325
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-07 21:30 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: