## Stem clausal$ (all stems)

### 20 papers:

- IJCAR-2014-NalonMD #confluence #logic
- Clausal Resolution for Modal Logics of Confluence (CN, JM, CD), pp. 322–336.
- SAT-2014-BelovHM #proving #using
- MUS Extraction Using Clausal Proofs (AB, MH, JMS), pp. 48–57.
- SAT-2014-WetzlerHH #named #performance #proving #using
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (NW, MH, WAHJ), pp. 422–429.
- SPLC-2010-Nakajima #automation #diagrams #encoding #feature model
- Non-clausal Encoding of Feature Diagram for Automated Diagnosis (SN), pp. 420–424.
- SAT-2010-KlieberSGC #learning
- A Non-prenex, Non-clausal QBF Solver with Game-State Learning (WK, SS, SG, EMC), pp. 128–142.
- DAC-2009-JainC #graph #performance #satisfiability #using
- Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts (HJ, EMC), pp. 563–568.
- CADE-2009-LahiriQ #abstraction #algorithm #complexity
- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction (SKL, SQ), pp. 214–229.
- SAT-2008-StachniakB #learning #satisfiability
- Speeding-Up Non-clausal Local Search for Propositional Satisfiability with Clause Learning (ZS, AB), pp. 257–270.
- SAT-2006-JainBC #satisfiability #using
- Satisfiability Checking of Non-clausal Formulas Using General Matings (HJ, CB, EMC), pp. 75–89.
- SAT-2004-ThiffaultBW
- Solving Non-clausal Formulas with DPLL search (CT, FB, TW), pp. 147–156.
- CADE-2002-GeorgievaHS #decidability
- A New Clausal Class Decidable by Hyperresolution (LG, UH, RAS), pp. 260–274.
- CSL-2002-Nivelle #normalisation #proving
- Extraction of Proofs from the Clausal Normal Form Transformation (HdN), pp. 584–598.
- SAT-2002-Stachniak
- Going non-clausal (ZS), p. 21.
- IJCAR-2001-Pliuskevicius
- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL (RP), pp. 107–120.
- ICLP-1991-Harland #logic programming #source code
- A Clausal Form for the Completion of Logic Programs (JH), pp. 711–725.
- ISLP-1991-Meyden #logic #specification
- A Clausal Logic for Deontic Action Specification (RvdM), pp. 221–238.
- CADE-1990-NieuwenhuisOR #implementation #named
- TRIP: An Implementation of Clausal Rewriting (RN, FO, AR), pp. 667–668.
- SLP-1985-Fribourg85 #interpreter #logic programming #named #programming language
- SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting (LF), pp. 172–184.
- CADE-1984-Gelder #calculus #satisfiability
- A Satisfiability Tester for Non-Clausal Propositional Calculus (AVG), pp. 101–112.
- ICALP-1983-HsiangD #proving #theorem proving
- Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.