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.