Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
35 | Christophe Jermann, Bertrand Neveu, Gilles Trombettoni |
A New Structural Rigidity for Geometric Constraint Systems. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
|
35 | Xiao-Shan Gao, Qiang Lin |
MMP/Geometer - A Software Package for Automated Geometric Reasoning. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
Geometry software, geometric theorem discovering, geometric diagram generation, intelligent dynamic geometry, automated reasoning, geometric theorem proving |
35 | Gábor Bodnár |
Algorithmic Tests for the Normal Crossing Property. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
|
35 | Mohamed Shalaby, Bert Jüttler, Josef Schicho |
C1 Spline Implicitization of Planar Curves. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
knot removal, approximation, B-spline, implicitization |
35 | Lu Yang |
Distance Coordinates Used in Geometric Constraint Solving. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
|
35 | John C. Owen, Steve C. Power |
The Nonsolvability by Radicals of Generic 3-connected Planar Graphs. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
|
35 | Solen Corvez, Fabrice Rouillier |
Using Computer Algebra Tools to Classify Serial Manipulators. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
|
35 | Dongming Wang 0001 |
GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
|
35 | Alexander A. Pasko, Valery Adzhiev |
Function-Based Shape Modeling: Mathematical Framework and Specialized Language. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
|
35 | Hongbo Li 0012 |
Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
Cayley algebra, bracket algebra, affine geometry, automated theorem proving, projective geometry, conics |
35 | Irina Tchoupaeva |
Analysis of Geometrical Theorems in Coordinate-Free Form by Using Anticommutative Gröbner Bases Method. |
Automated Deduction in Geometry |
2002 |
DBLP DOI BibTeX RDF |
|
35 | Jürgen Richter-Gebert, Dongming Wang 0001 (eds.) |
Automated Deduction in Geometry, Third International Workshop, ADG 2000, Zurich, Switzerland, September 25-27, 2000, Revised Papers |
Automated Deduction in Geometry |
2001 |
DBLP DOI BibTeX RDF |
|
35 | Xiao-Shan Gao, Lei-Dong Huang, Kun Jiang |
A Hybrid Method for Solving Geometric Constraint Problems. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Daniela Tulone, Chee-Keng Yap, Chen Li 0003 |
Randomized Zero Testing of Radical Expressions and Elementary Geometry Theorem Proving. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Christoph M. Hoffmann, Bo Yuan |
On Spatial Constraint Solving Approaches. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Fabrice Rouillier, Mohab Safey El Din, Éric Schost |
Solving the Birkhoff Interpolation Problem via the Critical Point Method: An Experimental Study. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Christophe Dehlinger, Jean-François Dufourd, Pascal Schreck |
Higher-Order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Michael Bulmer, Desmond Fearnley-Sander, Timothy Stokes 0001 |
The Kinds of Truth of Geometry Theorems. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Timothy F. Havel |
Qubit Logic, Algebra and Geometry. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Philippe Aubry, Dongming Wang 0001 |
Reasoning about Surfaces Using Differential Zero and Ideal Decomposition. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Ulrich Kortenkamp, Jürgen Richter-Gebert |
Decision Complexity in Dynamic Geometry. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Jacques D. Fleuriot |
Nonstandard Geometric Proofs. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Hongbo Li 0012, Yihong Wu 0002 |
Automated Theorem Proving in Incidence Geometry - A Bracket Algebra Based Elimination Method. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Ricardo Caferra, Nicolas Peltier, François Puitg |
Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
Automated geometric reasoning, model (counter-example) building, proof structuring with diagrams, analogy, computer assisted learning |
35 | Lu Yang, Ju Zhang |
A Practical Program of Automated Proving for a Class of Geometric Inequalities. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Pasqualina Conti, Carlo Traverso |
Algebraic and Semialgebraic Proofs: Methods and Paradoxes. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Laura Bazzotti, Giorgio Dalzotto, Lorenzo Robbiano |
Remarks on Geometric Theorem Proving. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Timothy Stokes 0001, Michael Bulmer |
A Complex Change of Variables for Geometrical Reasoning. |
Automated Deduction in Geometry |
2000 |
DBLP DOI BibTeX RDF |
|
35 | Xiao-Shan Gao, Dongming Wang 0001, Lu Yang (eds.) |
Automated Deduction in Geometry, Second International Workshop, ADG'98, Beijing, China, August 1-3, 1998, Proceedings |
Automated Deduction in Geometry |
1999 |
DBLP DOI BibTeX RDF |
|
35 | Chuan-Zhong Li, Jing-Zhong Zhang |
Readable Machine Solving in Geometry and ICAI Software MSG. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Lu Yang, Xiaorong Hou, Bican Xia |
Automated Discovering and Proving for Geometric Inequalities. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Haiquan Yang, Shugong Zhang, Guochen Feng |
A Clifford Algebraic Method for Geometric Reasoning. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Wu Wen-Tsün |
Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Andreas Dolzmann |
Solving Geometric Problems with Real Quantifier Elimination. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Hongbo Li |
Some Applications of Clifford Algebra to Geometries. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Jae Yeol Lee |
A 2D Geometric Constraint Solver for Parametric Design Using Graph Analysis and Reduction. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
variational design, constructive constraint solving, graph reduction, Parametric design |
35 | Desmond Fearnley-Sander |
Plane Euclidian Reasoning. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Zongying Ou, Jun Liu |
Variant Geometry Analysis and Synthesis in Mechanical CAD. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Thierry Boy de la Tour, Stéphane Fèvre, Dongming Wang 0001 |
Clifford Term Rewriting for Geometric Reasoning in 3D. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Didier Bondyfalat, Bernard Mourrain, Théodore Papadopoulo |
An Application of Automatic Theorem Proving in Computer Vision. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Jacques D. Fleuriot, Lawrence C. Paulson |
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Xiao-Shan Gao |
Automated Geometry Diagram Construction and Engineering Geometry. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Dongming Wang 0001 |
Decomposing Algebraic Varieties. |
Automated Deduction in Geometry |
1998 |
DBLP DOI BibTeX RDF |
|
34 | Peter Höfner, Georg Struth |
Automated Reasoning in Kleene Algebra. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
34 | Ashish Tiwari 0001, Sumit Gulwani |
Logical Interpretation: Static Program Analysis Using Theorem Proving. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
34 | Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv |
Labelled Clauses. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
34 | Ting Zhang 0001, Henny B. Sipma, Zohar Manna |
The Decidability of the First-Order Theory of Knuth-Bendix Order. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
34 | Konstantin Korovin, Andrei Voronkov |
An AC-Compatible Knuth-Bendix Order. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
34 | Hans de Nivelle |
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
34 | Christophe Ringeissen |
Matching in a Class of Combined Non-disjoint Theories. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
34 | Bernhard Gramlich, Reinhard Pichler |
Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
34 | Carsten Schürmann |
Tutorial: Meta-logical Frameworks. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
34 | Peter B. Andrews, Chad E. Brown |
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
34 | Enrico Giunchiglia, Armando Tacchella |
System Description: *SAT: A Platform for the Development of Modal Decision Procedures. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
34 | Peter Baumgartner 0001, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang 0001 |
Workshop: Model Computation - Principles, Algorithms, Applications. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
34 | Reinhard Pichler |
Solving Equational Problems Efficiently. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
34 | Karsten Konrad, David A. Wolfram |
System Description: Kimba, A Model Generator for Many-Valued First-Order Logics. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
34 | Stéphane Demri, Rajeev Goré |
Tractable Transformations from Modal Provability Logics into First-Order Logic. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
34 | Alexander Leitsch |
Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction. |
FTP (LNCS Selection) |
1998 |
DBLP DOI BibTeX RDF |
|
34 | Amir Pnueli |
Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
34 | Reinhold Letz |
Using Matings for Pruning Connection Tableaux. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
34 | Matthew Bishop, Peter B. Andrews |
Selectively Instantiating Definitions. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
34 | Christoph Kreitz, Mark Hayden, Jason Hickey |
A Proof Environment for the Development of Group Communication Systems. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
34 | Carsten Schürmann, Frank Pfenning |
Automated Theorem Proving in a Simple Meta-Logic for LF. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
34 | Maria Paola Bonacina |
The Clause-Diffusion Theorem Prover Peers-mcd (System Description). |
CADE |
1997 |
DBLP DOI BibTeX RDF |
|
34 | Saturnino F. Luz-Filho |
Grammar Specification in Categorial Logics and Theorem Proving. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
Mechanisms (semantic tableaux) and Applications (computational liguistics) |
34 | Peter Graf |
Path Indexing for AC-Theories. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
34 | Xiaorong Huang, Armin Fiedler |
Presenting Machine-Found Proofs. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
34 | Gernot Salzer |
Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
34 | David A. Basin, Seán Matthews |
Structuring Metatheory on Inductive Definitions. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
34 | Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach |
MUltlog 1.0: Towards an Expert System for Many-Valued Logics. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
34 | Jörg Denzinger, Stephan Schulz 0001 |
Learning Domain Knowledge to Improve Theorem Proving. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
34 | Peter Graf |
Extended Path-Indexing. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | Manfred Kerber, Michael Kohlhase |
A Mechanization of Strong Kleene Logic for Partial Functions. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | Xiaorong Huang |
Reconstruction Proofs at the Assertion Level. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | Frederic D. Portoraro |
Symlog: Automated Advice in Fitch-style Proof Construction. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | Robert Nieuwenhuis, Albert Rubio |
AC-Superposition with Constraints: No AC-Unifiers Needed. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | François Bronsard, Uday S. Reddy, Robert W. Hasker |
Induction using Term Orderings. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | Tie-Cheng Wang, Allen Goldberg |
KITP-93: An Automated Inference System for Program Analysis. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood |
Deductive Composition of Astronomical Software from Subroutine Libraries. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | Geoff Sutcliffe |
Linear-Input Subset Analysis. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
34 | Franz Oppacher, E. Suen |
Controlling Deduction with Proof Condensation and Heuristics. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
34 | Steven Greenbaum, A. Nagasaka, Paul O'Rorke, David A. Plaisted |
Comparison of Natural Deduction and Locking Resolution Implementations. |
CADE |
1982 |
DBLP DOI BibTeX RDF |
|
34 | Tomasz Pietrzykowski, Stan Matwin |
Exponential Improvement of Efficient Backtracking: A Strategy for Plan-Based Deduction. |
CADE |
1982 |
DBLP DOI BibTeX RDF |
|
31 | Nicolette Bonnette, Rajeev Goré |
A Labelled Sequent System for Tense Logic Kt. |
Australian Joint Conference on Artificial Intelligence |
1998 |
DBLP DOI BibTeX RDF |
labelled deductive system, lean deduction, sequent system, automated deduction, tense logic |
31 | Fernando Ferreira 0001, Gilda Ferreira |
Commuting Conversions vs. the Standard Conversions of the "Good" Connectives. |
Stud Logica |
2009 |
DBLP DOI BibTeX RDF |
commuting conversions, predicative quantifiers, Natural deduction |
31 | Mario Lischka, Yukiko Endo, Manuel Sánchez Cuenca |
Deductive policies with XACML. |
SWS |
2009 |
DBLP DOI BibTeX RDF |
xacml, deduction |
31 | Michael Leuschel |
A framework for the integration of partial evaluation and abstract interpretation of logic programs. |
ACM Trans. Program. Lang. Syst. |
2004 |
DBLP DOI BibTeX RDF |
logic programming, program transformation, abstract interpretation, partial evaluation, flow analysis, Partial deduction |
31 | Rajeev Goré, Phuong Thê Nguyên |
CardS4: Modal Theorem Proving on Java Smartcards. |
E-smart |
2001 |
DBLP DOI BibTeX RDF |
security of mobile code, modal deduction |
31 | Miquel Bofill, Guillem Godoy |
On the Completeness of Arbitrary Selection Strategies for Paramodulation. |
ICALP |
2001 |
DBLP DOI BibTeX RDF |
automated deduction |
31 | Makoto Suzuki, Toshiyasu Matsushima, Shigeichi Hirasawa |
On a Deductive Reasoning Model and Method for Uncertainty. |
ICTAI |
1999 |
DBLP DOI BibTeX RDF |
discrete data analysis, expert system, information theory, statistics, conditional probability, deduction, divergence, contingency table, multinomial distribution |
31 | Connie Loggia Ramsey, Victor R. Basili |
An Evaluation of Expert Systems for Software Engineering Management. |
IEEE Trans. Software Eng. |
1989 |
DBLP DOI BibTeX RDF |
expert systems evaluation, prototype expert systems, software engineering management, abnormal patterns, expert system methods, rule-based deduction, frame-based abduction, simple rules, performance evaluation, software engineering, expert systems, knowledge acquisition, knowledge acquisition, software project, bottom-up approach, top-down approach |
31 | Tadao Murata, Du Zhang |
A Predicate-Transition Net Model for Parallel Interpretation of Logic Programs. |
IEEE Trans. Software Eng. |
1988 |
DBLP DOI BibTeX RDF |
AND/OR parallelisms, deduction process, Horn clause logic programs, Petri nets, logic programming, communicating processes, fixpoint semantics, predicate/transition nets, relational operations |
31 | José Espírito Santo |
Refocusing Generalised Normalisation. |
CiE |
2007 |
DBLP DOI BibTeX RDF |
generalised elimination rules, multiarity, normalisation |
31 | Kentaro Kikuchi |
On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus. |
LPAR |
2006 |
DBLP DOI BibTeX RDF |
|
31 | Andreas Zeller |
When Abstraction Fails. |
CC |
2005 |
DBLP DOI BibTeX RDF |
|
31 | Kalyani K. Manchi, Xindong Wu 0001 |
Dynamic Refinement of Classification Rules. |
ICTAI |
2002 |
DBLP DOI BibTeX RDF |
|
31 | José Espírito Santo |
Revisiting the Correspondence between Cut Elimination and Normalisation. |
ICALP |
2000 |
DBLP DOI BibTeX RDF |
|
31 | Anna Mikhajlova, Joakim von Wright |
Proving Isomorphism of First-Order Logic Proof Systems in HOL. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
31 | Michael Leuschel, Danny De Schreye |
Logic Program Specialisation: How To Be More Specific. |
PLILP |
1996 |
DBLP DOI BibTeX RDF |
|