BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Australia
1 × Czech Republic
1 × Israel
1 × Poland
1 × Portugal
1 × Sweden
15 × USA
2 × Austria
2 × Canada
2 × Germany
2 × Japan
2 × United Kingdom
3 × Spain
4 × France
4 × Italy
Collaborated with:
L.Bachmair Z.Hanna Z.Manna J.Jouannaud S.Mitra A.Nadel J.W.Klop G.Sivakumar N.A.Josephson S.Kaplan D.A.Plaisted M.Okada J.Hsiang J.Katz L.Wolf M.P.Bonacina I.Tzameret E.C.Ellerman C.Kirchner R.Treinen C.Hoot N.Lindenstrauss Y.Lee J.Kalechstain V.Ryvchin J.Liu T.Hassner A.Blass Y.Gurevich J.E.Dawson R.Goré Y.Zarai T.Lavee
Talks about:
rewrit (15) program (8) termin (7) system (5) abstract (4) problem (4) order (4) infer (4) prove (3) proof (3)

Person: Nachum Dershowitz

DBLP DBLP: Dershowitz:Nachum

Facilitated 1 volumes:

RTA 1989Ed

Contributed to:

SAT 20152015
RTA-TLCA 20142014
CSL 20132013
ICDAR 20132013
CSL 20102010
IJCAR 20082008
ICALP 20072007
SAT 20072007
SAT 20062006
DATE 20052005
RTA 20052005
SAT 20052005
ICLP 20042004
LICS 20032003
RTA 19991999
RTA 19981998
RTA 19971997
ILPS 19951995
RTA 19951995
RTA 19931993
CADE 19921992
ICALP 19911991
RTA 19911991
ALP 19901990
ICALP 19891989
POPL 19891989
CADE 19881988
LICS 19881988
LICS 19871987
RTA 19871987
SLP 19871987
CADE 19861986
LICS 19861986
SLP 19861986
RTA 19851985
SLP 19851985
ILPC 19841984
ICALP 19831983
ICALP 19811981
ICSE 19811981
ICALP 19791979
ICSE 19781978
POPL 19771977
IJCAR 20182018

Wrote 51 papers:

Hints Revealed (JK, VR, ND), pp. 71–87.
RTA-TLCA-2014-LiuDJ #analysis #confluence
Confluence by Critical Pair Analysis (JL, ND, JPJ), pp. 287–302.
Res Publica: The Universal Model of Computation (ND), pp. 5–10.
OCR-Free Transcript Alignment (TH, LW, ND), pp. 1310–1314.
Integrating Copies Obtained from Old and New Preservation Efforts (YZ, TL, ND, LW), pp. 47–51.
CSL-2010-BlassDG #algorithm
Exact Exploration and Hanging Algorithms (AB, ND, YG), pp. 140–154.
IJCAR-2008-BonacinaD #canonical
Canonical Inference for Implicational Systems (MPB, ND), pp. 380–395.
IJCAR-2008-Dershowitz #exclamation
Canonicity! (ND), pp. 327–331.
ICALP-2007-DershowitzT #complexity #proving
Complexity of Propositional Proofs Under a Promise (ND, IT), pp. 291–302.
SAT-2007-DershowitzHN #comprehension #satisfiability #towards
Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver (ND, ZH, AN), pp. 287–293.
SAT-2006-DershowitzHN #algorithm #satisfiability #scalability
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction (ND, ZH, AN), pp. 36–41.
DATE-2005-KatzHD #bound #model checking
Space-Efficient Bounded Model Checking (JK, ZH, ND), pp. 686–687.
Open. Closed. Open (ND), pp. 376–393.
RTA-2005-DershowitzE #order
Leanest Quasi-orderings (ND, ECE), pp. 32–45.
SAT-2005-DershowitzHK #bound #model checking
Bounded Model Checking with QBF (ND, ZH, JK), pp. 408–414.
SAT-2005-DershowitzHN #heuristic #satisfiability
A Clause-Based Heuristic for SAT Solvers (ND, ZH, AN), pp. 46–60.
ICLP-2004-Dershowitz #abstraction #termination
Termination by Abstraction (ND), pp. 1–18.
Abstract Saturation-Based Inference (ND, CK), pp. 65–74.
Jeopardy (ND, SM), pp. 16–29.
RTA-1998-DershowitzT #database #online #problem
An On-line Problem Database (ND, RT), pp. 332–342.
Innocuous Constructor-Sharing Combinations (ND), pp. 202–216.
ILPS-1995-Dershowitz #semantics
Goal Solving as Operational Semantics (ND), pp. 3–17.
RTA-1995-DershowitzJK #problem
Problems in Rewriting III (ND, JPJ, JWK), pp. 457–471.
RTA-1993-DershowitzH #termination #topic
Topics in Termination (ND, CH), pp. 198–212.
RTA-1993-DershowitzJK #problem
More Problems in Rewriting (ND, JPJ, JWK), pp. 468–487.
CADE-1992-DershowitzMS #convergence #decidability
Decidable Matching for Convergent Systems (ND, SM, GS), pp. 589–602.
ICALP-1991-Dershowitz #horn clause #set
Cononical Sets of Horn Clauses (ND), pp. 267–278.
RTA-1991-DershowitzJK #problem
Open Problems in Rewriting (ND, JPJ, JWK), pp. 445–456.
ALP-1990-DershowitzL #concurrent
An Abstract Concurrent Machine for Rewriting (ND, NL), pp. 318–331.
ALP-1990-DershowitzMS #equation
Equation Solving in Conditional AC-Theories (ND, SM, GS), pp. 283–297.
ICALP-1989-DershowitzKP #infinity #normalisation
Infinite Normal Forms (ND, SK, DAP), pp. 249–262.
Rewrite, Rewrite, Rewrite, Rewrite, Rewrite (ND, SK), pp. 250–259.
CADE-1988-DershowitzOS #canonical #term rewriting
Canonical Conditional Rewrite Systems (ND, MO, GS), pp. 538–549.
LICS-1988-DershowitzO #term rewriting
Proof-Theoretic Techniques for Term Rewriting Theory (ND, MO), pp. 104–111.
LICS-1987-BachmairD #first-order #proving #theorem proving
Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
RTA-1987-BachmairD #congruence
Completion for Rewriting Modulo a Congruence (LB, ND), pp. 192–203.
SLP-1987-DershowitzL87 #debugging #deduction
Deductive Debugging (ND, YJL), pp. 298–306.
CADE-1986-BachmairD #termination
Commutation, Transformation, and Termination (LB, ND), pp. 5–20.
LICS-1986-BachmairDH #equation #order #proving
Orderings for Equational Proofs (LB, ND, JH), pp. 346–357.
SLP-1986-JosephsonD86 #implementation
An Implementation of Narrowing: The RITE Way (NAJ, ND), pp. 187–197.
RTA-1985-Dershowitz #termination
Termination (ND), pp. 180–224.
SLP-1985-DershowitzP85 #logic programming
Logic Programming cum Applicative Programming (ND, DAP), pp. 54–66.
ILPC-1984-DershowitzJ84 #logic programming
Logic Programming by Completion (ND, NAJ), pp. 313–320.
ICALP-1983-HsiangD #proving #theorem proving
Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.
ICALP-1981-Dershowitz #linear #term rewriting #termination
Termination of Linear Rewriting Systems (ND), pp. 448–458.
ICSE-1981-Dershowitz #abstraction #evolution #source code
The Evolution of Programs: Program Abstraction and Instantiation (ND), pp. 79–89.
ICALP-1979-DershowitzM #multi #order #proving #termination
Proving termination with Multiset Orderings (ND, ZM), pp. 188–202.
Inference Rules for Program Annotation (ND, ZM), pp. 158–167.
POPL-1977-DershowitzM #automation #evolution #source code
The Evolution of Programs: A System for Automatic Program Modification (ND, ZM), pp. 144–154.
TAPSOFT-1993-Dershowitz #termination
Trees, Ordinals and Termination (ND), pp. 243–250.
Well-Founded Unions (JED, ND, RG), pp. 117–133.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.